# HG changeset patch
# User wenzelm
# Date 876491532 -7200
# Node ID 9a5a4e123859a5a68adca90804a8aeca10189ae3
# Parent  278f0a1e5986f47a18d51b74e24110d5f90e5601
fixed dots;

diff -r 278f0a1e5986 -r 9a5a4e123859 src/FOL/FOL.ML
--- a/src/FOL/FOL.ML	Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/FOL.ML	Fri Oct 10 15:52:12 1997 +0200
@@ -22,14 +22,14 @@
 
 (*introduction rule involving only EX*)
 qed_goal "ex_classical" FOL.thy 
-   "( ~(EX x. P(x)) ==> P(a)) ==> EX x.P(x)"
+   "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)"
  (fn prems=>
   [ (rtac classical 1),
     (eresolve_tac (prems RL [exI]) 1) ]);
 
 (*version of above, simplifying ~EX to ALL~ *)
 qed_goal "exCI" FOL.thy 
-   "(ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)"
+   "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)"
  (fn [prem]=>
   [ (rtac ex_classical 1),
     (resolve_tac [notI RS allI RS prem] 1),
diff -r 278f0a1e5986 -r 9a5a4e123859 src/FOL/IFOL.ML
--- a/src/FOL/IFOL.ML	Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/IFOL.ML	Fri Oct 10 15:52:12 1997 +0200
@@ -26,12 +26,12 @@
  (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
 
 qed_goal "allE" IFOL.thy 
-    "[| ALL x.P(x); P(x) ==> R |] ==> R"
+    "[| ALL x. P(x); P(x) ==> R |] ==> R"
  (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
 
 (*Duplicates the quantifier; for use with eresolve_tac*)
 qed_goal "all_dupE" IFOL.thy 
-    "[| ALL x.P(x);  [| P(x); ALL x.P(x) |] ==> R \
+    "[| ALL x. P(x);  [| P(x); ALL x. P(x) |] ==> R \
 \    |] ==> R"
  (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
 
@@ -126,12 +126,12 @@
 
 (*Sometimes easier to use: the premises have no shared variables.  Safe!*)
 qed_goal "ex_ex1I" IFOL.thy
-    "[| EX x.P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"
+    "[| EX x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"
  (fn [ex,eq] => [ (rtac (ex RS exE) 1),
                   (REPEAT (ares_tac [ex1I,eq] 1)) ]);
 
 qed_goalw "ex1E" IFOL.thy [ex1_def]
-    "[| EX! x.P(x);  !!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R |] ==> R"
+    "[| EX! x. P(x);  !!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R |] ==> R"
  (fn prems =>
   [ (cut_facts_tac prems 1),
     (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ]);
@@ -194,21 +194,21 @@
       ORELSE  eresolve_tac [iffE,notE] 1)) ]);
 
 qed_goal "all_cong" IFOL.thy 
-    "(!!x.P(x) <-> Q(x)) ==> (ALL x.P(x)) <-> (ALL x.Q(x))"
+    "(!!x. P(x) <-> Q(x)) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
  (fn prems =>
   [ (REPEAT   (ares_tac [iffI,allI] 1
       ORELSE   mp_tac 1
       ORELSE   etac allE 1 ORELSE iff_tac prems 1)) ]);
 
 qed_goal "ex_cong" IFOL.thy 
-    "(!!x.P(x) <-> Q(x)) ==> (EX x.P(x)) <-> (EX x.Q(x))"
+    "(!!x. P(x) <-> Q(x)) ==> (EX x. P(x)) <-> (EX x. Q(x))"
  (fn prems =>
   [ (REPEAT   (etac exE 1 ORELSE ares_tac [iffI,exI] 1
       ORELSE   mp_tac 1
       ORELSE   iff_tac prems 1)) ]);
 
 qed_goal "ex1_cong" IFOL.thy 
-    "(!!x.P(x) <-> Q(x)) ==> (EX! x.P(x)) <-> (EX! x.Q(x))"
+    "(!!x. P(x) <-> Q(x)) ==> (EX! x. P(x)) <-> (EX! x. Q(x))"
  (fn prems =>
   [ (REPEAT   (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
       ORELSE   mp_tac 1
@@ -231,7 +231,7 @@
 
 (*A special case of ex1E that would otherwise need quantifier expansion*)
 qed_goal "ex1_equalsE" IFOL.thy
-    "[| EX! x.P(x);  P(a);  P(b) |] ==> a=b"
+    "[| EX! x. P(x);  P(a);  P(b) |] ==> a=b"
  (fn prems =>
   [ (cut_facts_tac prems 1),
     (etac ex1E 1),
@@ -352,13 +352,13 @@
 
 (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
 qed_goal "all_impE" IFOL.thy 
-    "[| (ALL x.P(x))-->S;  !!x.P(x);  S ==> R |] ==> R"
+    "[| (ALL x. P(x))-->S;  !!x. P(x);  S ==> R |] ==> R"
  (fn major::prems=>
   [ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]);
 
 (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
 qed_goal "ex_impE" IFOL.thy 
-    "[| (EX x.P(x))-->S;  P(x)-->S ==> R |] ==> R"
+    "[| (EX x. P(x))-->S;  P(x)-->S ==> R |] ==> R"
  (fn major::prems=>
   [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]);
 
diff -r 278f0a1e5986 -r 9a5a4e123859 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/IFOL.thy	Fri Oct 10 15:52:12 1997 +0200
@@ -96,11 +96,11 @@
 
   (* Quantifiers *)
 
-  allI          "(!!x. P(x)) ==> (ALL x.P(x))"
-  spec          "(ALL x.P(x)) ==> P(x)"
+  allI          "(!!x. P(x)) ==> (ALL x. P(x))"
+  spec          "(ALL x. P(x)) ==> P(x)"
 
-  exI           "P(x) ==> (EX x.P(x))"
-  exE           "[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"
+  exI           "P(x) ==> (EX x. P(x))"
+  exE           "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
 
   (* Reflection *)
 
diff -r 278f0a1e5986 -r 9a5a4e123859 src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/cladata.ML	Fri Oct 10 15:52:12 1997 +0200
@@ -25,7 +25,7 @@
 
 (*Better for fast_tac: needs no quantifier duplication!*)
 qed_goal "alt_ex1E" IFOL.thy
-    "[| EX! x.P(x);                                              \
+    "[| EX! x. P(x);                                              \
 \       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
 \    |] ==> R"
  (fn major::prems =>
diff -r 278f0a1e5986 -r 9a5a4e123859 src/FOL/ex/List.ML
--- a/src/FOL/ex/List.ML	Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/ex/List.ML	Fri Oct 10 15:52:12 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";
@@ -37,7 +37,7 @@
 by (IND_TAC list_ind Simp_tac "l" 1);
 qed "forall_app";
 
-goal List.thy "forall(l,%x.P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)";
+goal List.thy "forall(l,%x. P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)";
 by (IND_TAC list_ind Simp_tac "l" 1);
 by (Fast_tac 1);
 qed "forall_conj";
@@ -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 278f0a1e5986 -r 9a5a4e123859 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
diff -r 278f0a1e5986 -r 9a5a4e123859 src/FOL/ex/cla.ML
--- a/src/FOL/ex/cla.ML	Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/ex/cla.ML	Fri Oct 10 15:52:12 1997 +0200
@@ -127,22 +127,22 @@
 by (Blast_tac 1);
 result(); 
 
-goal FOL.thy "(EX x. P-->Q(x))  <->  (P --> (EX x.Q(x)))";
+goal FOL.thy "(EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
 by (Blast_tac 1);
 result(); 
 
-goal FOL.thy "(EX x.P(x)-->Q)  <->  (ALL x.P(x)) --> Q";
+goal FOL.thy "(EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
 by (Blast_tac 1);
 result(); 
 
-goal FOL.thy "(ALL x.P(x)) | Q  <->  (ALL x. P(x) | Q)";
+goal FOL.thy "(ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
 by (Blast_tac 1);
 result(); 
 
 (*Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux,
   JAR 10 (265-281), 1993.  Proof is trivial!*)
 goal FOL.thy
-    "~ ((EX x.~P(x)) & ((EX x.P(x)) | (EX x.P(x) & Q(x))) & ~ (EX x.P(x)))";
+    "~ ((EX x.~P(x)) & ((EX x. P(x)) | (EX x. P(x) & Q(x))) & ~ (EX x. P(x)))";
 by (Blast_tac 1);
 result();
 
@@ -207,7 +207,7 @@
 
 writeln"Problem 24";
 goal FOL.thy "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
-\    (~(EX x.P(x)) --> (EX x.Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
+\    (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
 \   --> (EX x. P(x)&R(x))";
 by (Blast_tac 1); 
 result();
@@ -240,7 +240,7 @@
 writeln"Problem 28.  AMENDED";
 goal FOL.thy "(ALL x. P(x) --> (ALL x. Q(x))) &   \
 \       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
-\       ((EX x.S(x)) --> (ALL x. L(x) --> M(x)))  \
+\       ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))  \
 \   --> (ALL x. P(x) & L(x) --> M(x))";
 by (Blast_tac 1);  
 result();
@@ -260,7 +260,7 @@
 result();
 
 writeln"Problem 31";
-goal FOL.thy "~(EX x.P(x) & (Q(x) | R(x))) & \
+goal FOL.thy "~(EX x. P(x) & (Q(x) | R(x))) & \
 \       (EX x. L(x) & P(x)) & \
 \       (ALL x. ~ R(x) --> M(x))  \
 \   --> (EX x. L(x) & M(x))";
@@ -306,7 +306,7 @@
 
 writeln"Problem 37";
 goal FOL.thy "(ALL z. EX w. ALL x. EX y. \
-\          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) & \
+\          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \
 \       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
 \       ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
 \   --> (ALL x. EX y. R(x,y))";
@@ -385,7 +385,7 @@
 (*Hard because it involves substitution for Vars;
   the type constraint ensures that x,y,z have the same type as a,b,u. *)
 goal FOL.thy "(EX x y::'a. ALL z. z=x | z=y) & P(a) & P(b) & a~=b \
-\               --> (ALL u::'a.P(u))";
+\               --> (ALL u::'a. P(u))";
 by Safe_tac;
 by (res_inst_tac [("x","a")] allE 1);
 by (assume_tac 1);
@@ -396,7 +396,7 @@
 
 writeln"Problem 50";  
 (*What has this to do with equality?*)
-goal FOL.thy "(ALL x. P(a,x) | (ALL y.P(x,y))) --> (EX x. ALL y.P(x,y))";
+goal FOL.thy "(ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
 by (Blast_tac 1);
 result();
 
diff -r 278f0a1e5986 -r 9a5a4e123859 src/FOL/ex/foundn.ML
--- a/src/FOL/ex/foundn.ML	Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/ex/foundn.ML	Fri Oct 10 15:52:12 1997 +0200
@@ -99,7 +99,7 @@
 
 
 (*Parallel lifting example. *)
-goal IFOL.thy "EX u.ALL x.EX v.ALL y.EX w. P(u,x,v,y,w)";
+goal IFOL.thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
 by (resolve_tac [exI, allI] 1);
 by (resolve_tac [exI, allI] 1);
 by (resolve_tac [exI, allI] 1);
@@ -108,7 +108,7 @@
 
 
 val prems =
-goal IFOL.thy "(EX z.F(z)) & B ==> (EX z. F(z) & B)";
+goal IFOL.thy "(EX z. F(z)) & B ==> (EX z. F(z) & B)";
 by (rtac conjE 1);
 by (resolve_tac prems 1);
 by (rtac exE 1);
diff -r 278f0a1e5986 -r 9a5a4e123859 src/FOL/ex/int.ML
--- a/src/FOL/ex/int.ML	Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/ex/int.ML	Fri Oct 10 15:52:12 1997 +0200
@@ -211,11 +211,11 @@
 
 writeln"The converse is classical in the following implications...";
 
-goal IFOL.thy "(EX x.P(x)-->Q)  -->  (ALL x.P(x)) --> Q";
+goal IFOL.thy "(EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q";
 by (IntPr.fast_tac 1); 
 result();  
 
-goal IFOL.thy "((ALL x.P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
+goal IFOL.thy "((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
 by (IntPr.fast_tac 1); 
 result();  
 
@@ -223,7 +223,7 @@
 by (IntPr.fast_tac 1); 
 result();  
 
-goal IFOL.thy "(ALL x.P(x)) | Q  -->  (ALL x. P(x) | Q)";
+goal IFOL.thy "(ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)";
 by (IntPr.fast_tac 1); 
 result();  
 
@@ -237,15 +237,15 @@
 writeln"The following are not constructively valid!";
 (*The attempt to prove them terminates quickly!*)
 
-goal IFOL.thy "((ALL x.P(x))-->Q) --> (EX x.P(x)-->Q)";
+goal IFOL.thy "((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)";
 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
 getgoal 1; 
 
-goal IFOL.thy "(P --> (EX x.Q(x))) --> (EX x. P-->Q(x))";
+goal IFOL.thy "(P --> (EX x. Q(x))) --> (EX x. P-->Q(x))";
 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
 getgoal 1; 
 
-goal IFOL.thy "(ALL x. P(x) | Q) --> ((ALL x.P(x)) | Q)";
+goal IFOL.thy "(ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)";
 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
 getgoal 1; 
 
@@ -294,7 +294,7 @@
 
 writeln"Problem 24";
 goal IFOL.thy "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
-\    (~(EX x.P(x)) --> (EX x.Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
+\    (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
 \   --> ~~(EX x. P(x)&R(x))";
 (*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
 by IntPr.safe_tac; 
@@ -330,7 +330,7 @@
 writeln"Problem ~~28.  AMENDED";
 goal IFOL.thy "(ALL x. P(x) --> (ALL x. Q(x))) &   \
 \       (~~(ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
-\       (~~(EX x.S(x)) --> (ALL x. L(x) --> M(x)))  \
+\       (~~(EX x. S(x)) --> (ALL x. L(x) --> M(x)))  \
 \   --> (ALL x. P(x) & L(x) --> M(x))";
 by (IntPr.fast_tac 1);  (*48 secs*)
 result();
@@ -350,7 +350,7 @@
 result();
 
 writeln"Problem 31";
-goal IFOL.thy "~(EX x.P(x) & (Q(x) | R(x))) & \
+goal IFOL.thy "~(EX x. P(x) & (Q(x) | R(x))) & \
 \       (EX x. L(x) & P(x)) & \
 \       (ALL x. ~ R(x) --> M(x))  \
 \   --> (EX x. L(x) & M(x))";
@@ -384,7 +384,7 @@
 writeln"Problem 37";
 goal IFOL.thy
        "(ALL z. EX w. ALL x. EX y. \
-\          ~~(P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) & \
+\          ~~(P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \
 \       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
 \       (~~(EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
 \   --> ~~(ALL x. EX y. R(x,y))";
diff -r 278f0a1e5986 -r 9a5a4e123859 src/FOL/ex/intro.ML
--- a/src/FOL/ex/intro.ML	Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/ex/intro.ML	Fri Oct 10 15:52:12 1997 +0200
@@ -32,7 +32,7 @@
 result();
 
 (*Correct version, delaying use of "spec" until last*)
-goal FOL.thy "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
+goal FOL.thy "(ALL x y. P(x,y))  -->  (ALL z w. P(w,z))";
 by (rtac impI 1);
 by (rtac allI 1);
 by (rtac allI 1);
diff -r 278f0a1e5986 -r 9a5a4e123859 src/FOL/ex/mini.ML
--- a/src/FOL/ex/mini.ML	Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/ex/mini.ML	Fri Oct 10 15:52:12 1997 +0200
@@ -26,8 +26,8 @@
                   ["~(P&Q) <-> ~P | ~Q",
                    "~(P|Q) <-> ~P & ~Q",
                    "~~P <-> P",
-                   "~(ALL x.P(x)) <-> (EX x. ~P(x))",
-                   "~(EX x.P(x)) <-> (ALL x. ~P(x))"];
+                   "~(ALL x. P(x)) <-> (EX x. ~P(x))",
+                   "~(EX x. P(x)) <-> (ALL x. ~P(x))"];
 
 (*** Removal of --> and <-> (positive and negative occurrences) ***)
 (*Last one is important for computing a compact CNF*)
@@ -43,21 +43,21 @@
 
 val ex_simps = map prove_fun 
                 ["(EX x. P) <-> P",
-                 "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q",
-                 "(EX x. P & Q(x)) <-> P & (EX x.Q(x))",
-                 "(EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))",
-                 "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q",
-                 "(EX x. P | Q(x)) <-> P | (EX x.Q(x))"];
+                 "(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
+                 "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
+                 "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))",
+                 "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
+                 "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"];
 
 (*** Pushing in the universal quantifiers ***)
 
 val all_simps = map prove_fun
                 ["(ALL x. P) <-> P",
-                 "(ALL x. P(x) & Q(x)) <-> (ALL x.P(x)) & (ALL x.Q(x))",
-                 "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
-                 "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))",
-                 "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q",
-                 "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))"];
+                 "(ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))",
+                 "(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
+                 "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
+                 "(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
+                 "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
 
 
 val mini_ss=FOL_basic_ss addsimps (demorgans @ nnf_simps @ ex_simps @ all_simps);
diff -r 278f0a1e5986 -r 9a5a4e123859 src/FOL/ex/quant.ML
--- a/src/FOL/ex/quant.ML	Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/ex/quant.ML	Fri Oct 10 15:52:12 1997 +0200
@@ -9,40 +9,40 @@
 
 writeln"File FOL/ex/quant.";
 
-goal thy "(ALL x y.P(x,y))  -->  (ALL y x.P(x,y))";
+goal thy "(ALL x y. P(x,y))  -->  (ALL y x. P(x,y))";
 by tac;
 result();  
 
 
-goal thy "(EX x y.P(x,y)) --> (EX y x.P(x,y))";
+goal thy "(EX x y. P(x,y)) --> (EX y x. P(x,y))";
 by tac;
 result();  
 
 
 (*Converse is false*)
-goal thy "(ALL x.P(x)) | (ALL x.Q(x)) --> (ALL x. P(x) | Q(x))";
+goal thy "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
 by tac;
 result();  
 
-goal thy "(ALL x. P-->Q(x))  <->  (P--> (ALL x.Q(x)))";
+goal thy "(ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))";
 by tac;
 result();  
 
 
-goal thy "(ALL x.P(x)-->Q)  <->  ((EX x.P(x)) --> Q)";
+goal thy "(ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
 by tac;
 result();  
 
 
 writeln"Some harder ones";
 
-goal thy "(EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))";
+goal thy "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
 by tac;
 result();  
 (*6 secs*)
 
 (*Converse is false*)
-goal thy "(EX x. P(x)&Q(x)) --> (EX x.P(x))  &  (EX x.Q(x))";
+goal thy "(EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))";
 by tac;
 result();  
 
@@ -70,26 +70,26 @@
 by tac handle ERROR => writeln"Failed, as expected";  
 getgoal 1; 
 
-goal thy "P(?a) --> (ALL x.P(x))";
+goal thy "P(?a) --> (ALL x. P(x))";
 by tac handle ERROR => writeln"Failed, as expected";
 (*Check that subgoals remain: proof failed.*)
 getgoal 1;  
 
 goal thy
-    "(P(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))";
+    "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
 by tac handle ERROR => writeln"Failed, as expected";
 getgoal 1;  
 
 
 writeln"Back to things that are provable...";
 
-goal thy "(ALL x.P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))";
+goal thy "(ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
 by tac;  
 result();  
 
 
 (*An example of why exI should be delayed as long as possible*)
-goal thy "(P --> (EX x.Q(x))) & P --> (EX x.Q(x))";
+goal thy "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
 by tac;  
 result();  
 
diff -r 278f0a1e5986 -r 9a5a4e123859 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/simpdata.ML	Fri Oct 10 15:52:12 1997 +0200
@@ -42,7 +42,7 @@
   "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
 
 val quant_simps = map int_prove_fun
- ["(ALL x.P) <-> P",    "(EX x.P) <-> P"];
+ ["(ALL x. P) <-> P",    "(EX x. P) <-> P"];
 
 (*These are NOT supplied by default!*)
 val distrib_simps  = map int_prove_fun
@@ -103,23 +103,23 @@
 val ex_simps = map prove_fun 
                 ["(EX x. x=t & P(x)) <-> P(t)",
                  "(EX x. t=x & P(x)) <-> P(t)",
-                 "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q",
-                 "(EX x. P & Q(x)) <-> P & (EX x.Q(x))",
-                 "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q",
-                 "(EX x. P | Q(x)) <-> P | (EX x.Q(x))",
-                 "(EX x. P(x) --> Q) <-> (ALL x.P(x)) --> Q",
-                 "(EX x. P --> Q(x)) <-> P --> (EX x.Q(x))"];
+                 "(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
+                 "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
+                 "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
+                 "(EX x. P | Q(x)) <-> P | (EX x. Q(x))",
+                 "(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
+                 "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
 
 (*Miniscoping: pushing in universal quantifiers*)
 val all_simps = map prove_fun
                 ["(ALL x. x=t --> P(x)) <-> P(t)",
                  "(ALL x. t=x --> P(x)) <-> P(t)",
-                 "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
-                 "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))",
-                 "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q",
-                 "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))",
-                 "(ALL x. P(x) --> Q) <-> (EX x.P(x)) --> Q",
-                 "(ALL x. P --> Q(x)) <-> P --> (ALL x.Q(x))"];
+                 "(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
+                 "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
+                 "(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
+                 "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))",
+                 "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
+                 "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
 
 fun int_prove nm thm  = qed_goal nm IFOL.thy thm
     (fn prems => [ (cut_facts_tac prems 1), 
@@ -150,9 +150,9 @@
 
 prove     "not_iff" "~(P <-> Q) <-> (P <-> ~Q)";
 
-prove     "not_all" "(~ (ALL x.P(x))) <-> (EX x.~P(x))";
-prove     "imp_all" "((ALL x.P(x)) --> Q) <-> (EX x.P(x) --> Q)";
-int_prove "not_ex"  "(~ (EX x.P(x))) <-> (ALL x.~P(x))";
+prove     "not_all" "(~ (ALL x. P(x))) <-> (EX x.~P(x))";
+prove     "imp_all" "((ALL x. P(x)) --> Q) <-> (EX x. P(x) --> Q)";
+int_prove "not_ex"  "(~ (EX x. P(x))) <-> (ALL x.~P(x))";
 int_prove "imp_ex" "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)";
 
 int_prove "ex_disj_distrib"
diff -r 278f0a1e5986 -r 9a5a4e123859 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Fri Oct 10 15:51:38 1997 +0200
+++ b/src/Provers/splitter.ML	Fri Oct 10 15:52:12 1997 +0200
@@ -32,7 +32,7 @@
 val lift =
   let val ct = read_cterm (#sign(rep_thm iffD))
            ("[| !!x::'b::logic. Q(x) == R(x) |] ==> \
-            \P(%x.Q(x)) == P(%x.R(x))::'a::logic",propT)
+            \P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT)
   in prove_goalw_cterm [] ct
      (fn [prem] => [rewtac prem, rtac reflexive_thm 1])
   end;