# HG changeset patch
# User wenzelm
# Date 877102744 -7200
# Node ID ca23ee574faa4cd581e9faa7696be7fe515196c2
# Parent  e88ea232977ced6cea1fd56d25cb6627a20a27c0
tuned "." syntax;

diff -r e88ea232977c -r ca23ee574faa src/FOL/ex/List.ML
--- a/src/FOL/ex/List.ML	Fri Oct 17 17:33:22 1997 +0200
+++ b/src/FOL/ex/List.ML	Fri Oct 17 17:39:04 1997 +0200
@@ -8,7 +8,7 @@
 
 open List;
 
-val prems = goal List.thy "[| P([]);  !!x l. P(x. l) |] ==> All(P)";
+val prems = goal List.thy "[| P([]);  !!x l. P(x . l) |] ==> All(P)";
 by (rtac list_ind 1);
 by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
 qed "list_exh";
@@ -59,7 +59,7 @@
 by (ALL_IND_TAC nat_exh Asm_simp_tac 1);
 qed "at_app1";
 
-goal List.thy "at(l1++(x. l2), len(l1)) = x";
+goal List.thy "at(l1++(x . l2), len(l1)) = x";
 by (IND_TAC list_ind Simp_tac "l1" 1);
 qed "at_app_hd2";
 
diff -r e88ea232977c -r ca23ee574faa src/FOL/ex/List.thy
--- a/src/FOL/ex/List.thy	Fri Oct 17 17:33:22 1997 +0200
+++ b/src/FOL/ex/List.thy	Fri Oct 17 17:39:04 1997 +0200
@@ -17,33 +17,33 @@
    forall       :: ['a list, 'a => o] => o  
    len          :: 'a list => nat  
    at           :: ['a list, nat] => 'a  
-   "[]"         :: ('a list)                         ("[]")
-   "."          :: ['a, 'a list] => 'a list          (infixr 80)
+   Nil          :: ('a list)                         ("[]")
+   Cons         :: ['a, 'a list] => 'a list          (infixr "." 80)
    "++"         :: ['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