Def P  Q == (P  Q) & (P  Q)

is mentioned by

Thm* 'a:S, n:, f:('a'a), x:'a. Thm* (fun:('a). simp_rec_rel(fun,x,f,n)) Thm*  Thm* simp_rec_fun(x,f,n,0) = x Thm* & (m:. m<n  simp_rec_fun(x,f,n,m+1) = f(simp_rec_fun(x,f,n,m)))	[simp_rec_fun_lemma]
Thm* m,n:. m<n+1  m = n  m<n	[less_thm]
Thm* m,n:. m+1 = n+1    m = n	[inv_suc_eq]
Thm* (P  P)  True	[iff_refl]

In prior sections: core fun 1 well fnd int 1 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