Def A == A  False

is mentioned by

Thm* n,m:. n+1m  mn	[not_suc_less_eq]
Thm* P:(). (n:. P(n))  (n:. P(n) & (m:. m<n  P(m)))	[wop]
Thm* n,m:. n+n+1 = m+m	[not_odd_eq_even]
Thm* m,n:. m<n  n<m+1	[less_suc_not]
Thm* m,n:. m<n  nm	[not_less]
Thm* m,n:. (m<n & nm)	[less_eq_antisym]
Thm* m,n:. n = 0    m<m+n	[less_add_nonzero]
Thm* m,n:. m<n & m = n  n<m	[less_cases_imp]
Thm* m,n:. m<n & n = m+1    m+1<n	[less_not_suc]
Thm* m,n:. m<n & m+1 = n    m+1<n	[less_suc_eq_cor]
Thm* 'a:S, f:('a), x1,x2:'a. f(x1) & f(x2)  x1 = x2	[fun_eq_lemma]
Thm* m,n:. (m<n & n<m+1)	[less_less_suc]
Thm* m,n:. (m<n & n<m)	[less_antisym]

In prior sections: core bool 1 hol hol bool hol num hol prim rec int 2 hol arithmetic 3

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