Def A == A  False

is mentioned by

Thm* m,n:. m<n  m = n	[less_not_eq]
Thm* m,n:. m = n  m<n	[not_less_eq]
Thm* n:. n+1 = n	[suc_id]
Thm* m,n:. m<n+1  m = n  m<n	[less_suc_imp]
Thm* n:. n<0	[not_less_0]
Thm* n:. n<n	[less_refl]

In prior sections: core bool 1 hol hol bool hol num

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html