PrintForm Definitions hol prim rec Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hsimp rec fun wd
  'a:S. 
  all
  (x:'a. all
  (x:'a. (f:'a  'a. all
  (x:'a. (f:'a  'a. (n:hnum. equal
  (x:'a. (f:'a  'a. (n:hnum. (simp_rec_fun(x,f,n)
  (x:'a. (f:'a  'a. (n:hnum. ,select
  (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. simp_rec_rel
  (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. (fun
  (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. ,x
  (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. ,f
  (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. ,n))))))
By: Unab [`hsimp_rec_fun`] THEN StrongAuto THEN Simpsetp [`hol_to_nuprl`;`bequal`]
THEN
StrongAuto
THEN
Try (Complete (Unfold `label` 0))

Generated subgoals:

None

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

PrintForm Definitions hol prim rec Sections HOLlib Doc