Def P  Q == PQ

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, l:'a List, P:('a). every(P;l)  (n:. n<||l||  P(l[n]))	[every_el]
Thm* 'a:S, l:'a List. mt(l)  cons(head(l); tl(l)) = l	[cons_char]
Thm* 'a:S, h1,h2:'a. Thm* h1 = h2  (l1,l2:'a List. l1 = l2  cons(h1; l1) = cons(h2; l2))	[eq_list]
Thm* 'a:S, h1,h2:'a. h1 = h2  (l1,l2:'a List. cons(h1; l1) = cons(h2; l2))	[not_eq_list]
Thm* 'a:S, l1,l2:'a List. l1 = l2  (h1,h2:'a. cons(h1; l1) = cons(h2; l2))	[list_not_eq]
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]
Thm* 'b,'a:S, x:'b, f:('b'a('a List)'b). Thm* (fn1:(('a List)'b).  Thm* (fn1(nil) = x & (h:'a, t:'a List. fn1(cons(h; t)) = f(fn1(t),h,t))) Thm* & (fn1,y:(('a List)'b). Thm* & (fn1(nil) = x & (h:'a, t:'a List. fn1(cons(h; t)) = f(fn1(t),h,t)) Thm* & (& y(nil) = x Thm* & (& (h:'a, t:'a List. y(cons(h; t)) = f(y(t),h,t)) Thm* & ( Thm* & (fn1 = y)	[list_axiom]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 hol hol bool hol num hol prim rec hol arithmetic 1 hol list 1 hol restr binder

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