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 wf
  'a:S. simp_rec_fun  ('a  ('a  'a)  hnum  hnum  'a)
By: Unfolds [`hsimp_rec_fun`] 0 THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

None

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

PrintForm Definitions hol prim rec Sections HOLlib Doc