(2steps total) PrintForm Definitions FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: prime mset complete wf
  f:(Prime). prime_mset_complete(f)  
By: Def of prime_mset_complete(<term>)

Generated subgoal:

1 1. f : Prime
2. x : 
  if is_prime(x) f(x) else 0 fi  
1 step

About:
ifthenelsenatural_numberapplyfunctionmemberall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(2steps total) PrintForm Definitions FTA Sections DiscrMathExt Doc