PrintForm Definitions Lemmas hol prim rec Sections HOLlib Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: simp rec fun lemma
  'a:S, n:, f:('a'a), x:'a.
  (fun:('a). simp_rec_rel(fun,x,f,n))
  
  simp_rec_fun(x,f,n,0) = x
  & (m:. m<n  simp_rec_fun(x,f,n,m+1) = f(simp_rec_fun(x,f,n,m)))
By: RewriteOfThm Thm: hsimp rec fun lemma (SimpsetC [`hol_to_nuprl`;`bequal`])
THEN
Try (Complete (Unfold `hnum` 0))

Generated subgoals:

None

About:
assertnatural_numberaddless_thanapplyfunction
equalimpliesandall
exists
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions Lemmas hol prim rec Sections HOLlib Search Doc