PrintForm
Definitions
hol
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:
eq
pred
inc
'a
:Type. eq(
'a
)
(
'a
'a
)
By:
Unab [`subtype`;`eq_pred`] THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
hol
Sections
HOLlib
Search
Doc
'a:Type. eq('a) 
('a
'a
) 'a:Type. eq('a) ('a'a)
