src/FOL/ex/List.thy

--- a/src/FOL/ex/List.thy	Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/ex/List.thy	Fri Oct 10 15:52:12 1997 +0200
@@ -22,28 +22,28 @@
    "++"         :: ['a list, 'a list] => 'a list     (infixr 70)
 
 rules
- list_ind "[| P([]);  ALL x l. P(l)-->P(x.l) |] ==> All(P)"
+ list_ind "[| P([]);  ALL x l. P(l)-->P(x. l) |] ==> All(P)"
 
  forall_cong 
   "[| l = l';  !!x. P(x)<->P'(x) |] ==> forall(l,P) <-> forall(l',P')"
 
- list_distinct1 "~[] = x.l"
- list_distinct2 "~x.l = []"
+ list_distinct1 "~[] = x. l"
+ list_distinct2 "~x. l = []"
 
- list_free      "x.l = x'.l' <-> x=x' & l=l'"
+ list_free      "x. l = x'. l' <-> x=x' & l=l'"
 
  app_nil        "[]++l = l"
- app_cons       "(x.l)++l' = x.(l++l')"
- tl_eq  "tl(m.q) = q"
- hd_eq  "hd(m.q) = m"
+ app_cons       "(x. l)++l' = x.(l++l')"
+ tl_eq  "tl(m. q) = q"
+ hd_eq  "hd(m. q) = m"
 
  forall_nil "forall([],P)"
- forall_cons "forall(x.l,P) <-> P(x) & forall(l,P)"
+ forall_cons "forall(x. l,P) <-> P(x) & forall(l,P)"
 
  len_nil "len([]) = 0"
- len_cons "len(m.q) = succ(len(q))"
+ len_cons "len(m. q) = succ(len(q))"
 
- at_0 "at(m.q,0) = m"
- at_succ "at(m.q,succ(n)) = at(q,n)"
+ at_0 "at(m. q,0) = m"
+ at_succ "at(m. q,succ(n)) = at(q,n)"
 
 end