Def  == Unit+Unit

is mentioned by

Thm* 'a:S, P:(('a List)). (l:'a List. ||l|| = 0    P(l))  P(nil)	[length_eq_nil]
Thm* 'a:S, P:(('a List)), n:. Thm* (l:'a List. ||l|| = n+1    P(l)) Thm*  Thm* (l:'a List. ||l|| = n    (x:'a. P(cons(x; l))))	[length_eq_cons]
Thm* 'a:S, Q,P:('a), l:'a List. Thm* every(x:'a. (P(x))(Q(x));l)  every(P;l) & every(Q;l)	[every_conj]
Thm* 'a:S, Q,P:('a), l:'a List. Thm* every(x:'a. (P(x))(Q(x));l) = (every(P;l)every(Q;l))	[every_conj_2]
Thm* 'a:S, l:'a List, P:('a). every(P;l)  (n:. n<||l||  P(l[n]))	[every_el]
Thm* 'a:S, P:(('a List)). Thm* P(nil) & (t:'a List. P(t)  (h:'a. P(cons(h; t))))  (l:'a List. P(l))	[list_induct]

In prior sections: bool 1 list 1 hol hol bool hol num hol arithmetic 1 hol list 1 hol min hol pair hol restr binder

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