# HG changeset patch
# User wenzelm
# Date 876493781 -7200
# Node ID f1a1817659e628cb255010593174ce987e8c0239
# Parent  9a5a4e123859a5a68adca90804a8aeca10189ae3
fixed dots;

diff -r 9a5a4e123859 -r f1a1817659e6 src/Cube/ex/ex.ML
--- a/src/Cube/ex/ex.ML	Fri Oct 10 15:52:12 1997 +0200
+++ b/src/Cube/ex/ex.ML	Fri Oct 10 16:29:41 1997 +0200
@@ -19,37 +19,37 @@
 by (DEPTH_SOLVE (ares_tac simple 1));
 uresult();
 
-goal thy "A:* |- Lam a:A.a : ?T";
+goal thy "A:* |- Lam a:A. a : ?T";
 by (DEPTH_SOLVE (ares_tac simple 1));
 uresult();
 
-goal thy "A:* B:* b:B |- Lam x:A.b : ?T";
+goal thy "A:* B:* b:B |- Lam x:A. b : ?T";
 by (DEPTH_SOLVE (ares_tac simple 1));
 uresult();
 
-goal thy "A:* b:A |- (Lam a:A.a)^b: ?T";
+goal thy "A:* b:A |- (Lam a:A. a)^b: ?T";
 by (DEPTH_SOLVE (ares_tac simple 1));
 uresult();
 
-goal thy "A:* B:* c:A b:B |- (Lam x:A.b)^ c: ?T";
+goal thy "A:* B:* c:A b:B |- (Lam x:A. b)^ c: ?T";
 by (DEPTH_SOLVE (ares_tac simple 1));
 uresult();
 
-goal thy "A:* B:* |- Lam a:A.Lam b:B.a : ?T";
+goal thy "A:* B:* |- Lam a:A. Lam b:B. a : ?T";
 by (DEPTH_SOLVE (ares_tac simple 1));
 uresult();
 
 (* SECOND-ORDER TYPES *)
 
-goal L2_thy "|- Lam A:*. Lam a:A.a : ?T";
+goal L2_thy "|- Lam A:*. Lam a:A. a : ?T";
 by (DEPTH_SOLVE (ares_tac L2 1));
 uresult();
 
-goal L2_thy "A:* |- (Lam B:*.Lam b:B.b)^A : ?T";
+goal L2_thy "A:* |- (Lam B:*.Lam b:B. b)^A : ?T";
 by (DEPTH_SOLVE (ares_tac L2 1));
 uresult();
 
-goal L2_thy "A:* b:A |- (Lam B:*.Lam b:B.b) ^ A ^ b: ?T";
+goal L2_thy "A:* b:A |- (Lam B:*.Lam b:B. b) ^ A ^ b: ?T";
 by (DEPTH_SOLVE (ares_tac L2 1));
 uresult();
 
@@ -67,7 +67,7 @@
 by (DEPTH_SOLVE (ares_tac Lomega 1));
 uresult();
 
-goal Lomega_thy "B:* b:B |- (Lam y:B.b): ?T";
+goal Lomega_thy "B:* b:B |- (Lam y:B. b): ?T";
 by (DEPTH_SOLVE (ares_tac Lomega 1));
 uresult();
 
@@ -89,28 +89,28 @@
 by (DEPTH_SOLVE (ares_tac LP 1));
 uresult();
 
-goal LP_thy "A:* P:A->A->* a:A |- Pi a:A.P^a^a: ?T";
+goal LP_thy "A:* P:A->A->* a:A |- Pi a:A. P^a^a: ?T";
 by (DEPTH_SOLVE (ares_tac LP 1));
 uresult();
 
-goal LP_thy "A:* P:A->* Q:A->* |- Pi a:A.P^a -> Q^a: ?T";
+goal LP_thy "A:* P:A->* Q:A->* |- Pi a:A. P^a -> Q^a: ?T";
 by (DEPTH_SOLVE (ares_tac LP 1));
 uresult();
 
-goal LP_thy "A:* P:A->* |- Pi a:A.P^a -> P^a: ?T";
+goal LP_thy "A:* P:A->* |- Pi a:A. P^a -> P^a: ?T";
 by (DEPTH_SOLVE (ares_tac LP 1));
 uresult();
 
-goal LP_thy "A:* P:A->* |- Lam a:A.Lam x:P^a.x: ?T";
+goal LP_thy "A:* P:A->* |- Lam a:A. Lam x:P^a. x: ?T";
 by (DEPTH_SOLVE (ares_tac LP 1));
 uresult();
 
-goal LP_thy "A:* P:A->* Q:* |- (Pi a:A.P^a->Q) -> (Pi a:A.P^a) -> Q : ?T";
+goal LP_thy "A:* P:A->* Q:* |- (Pi a:A. P^a->Q) -> (Pi a:A. P^a) -> Q : ?T";
 by (DEPTH_SOLVE (ares_tac LP 1));
 uresult();
 
 goal LP_thy "A:* P:A->* Q:* a0:A |- \
-\       Lam x:Pi a:A.P^a->Q. Lam y:Pi a:A.P^a. x^a0^(y^a0): ?T";
+\       Lam x:Pi a:A. P^a->Q. Lam y:Pi a:A. P^a. x^a0^(y^a0): ?T";
 by (DEPTH_SOLVE (ares_tac LP 1));
 uresult();
 
@@ -124,7 +124,7 @@
 by (DEPTH_SOLVE (ares_tac LOmega 1));
 uresult();
 
-goal LOmega_thy "|- Lam A:*.Lam B:*.Lam x:A.Lam y:B.x : ?T";
+goal LOmega_thy "|- Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T";
 by (DEPTH_SOLVE (ares_tac LOmega 1));
 uresult();
 
@@ -148,18 +148,18 @@
 
 (* Second-order Predicate Logic *)
 
-goal LP2_thy "A:* P:A->* |- Lam a:A.P^a->(Pi A:*.A) : ?T";
+goal LP2_thy "A:* P:A->* |- Lam a:A. P^a->(Pi A:*.A) : ?T";
 by (DEPTH_SOLVE (ares_tac LP2 1));
 uresult();
 
 goal LP2_thy "A:* P:A->A->* |- \
-\       (Pi a:A.Pi b:A.P^a^b->P^b^a->Pi P:*.P) -> Pi a:A.P^a^a->Pi P:*.P : ?T";
+\       (Pi a:A. Pi b:A. P^a^b->P^b^a->Pi P:*.P) -> Pi a:A. P^a^a->Pi P:*.P : ?T";
 by (DEPTH_SOLVE (ares_tac LP2 1));
 uresult();
 
 (* Antisymmetry implies irreflexivity: *)
 goal LP2_thy "A:* P:A->A->* |- \
-\       ?p: (Pi a:A.Pi b:A.P^a^b->P^b^a->Pi P:*.P) -> Pi a:A.P^a^a->Pi P:*.P";
+\       ?p: (Pi a:A. Pi b:A. P^a^b->P^b^a->Pi P:*.P) -> Pi a:A. P^a^a->Pi P:*.P";
 by (strip_asms_tac LP2 1);
 by (rtac lam_ss 1);
 by (DEPTH_SOLVE_1(ares_tac LP2 1));
@@ -175,25 +175,25 @@
 
 (* LPomega *)
 
-goal LPomega_thy "A:* |- Lam P:A->A->*.Lam a:A.P^a^a : ?T";
+goal LPomega_thy "A:* |- Lam P:A->A->*.Lam a:A. P^a^a : ?T";
 by (DEPTH_SOLVE (ares_tac LPomega 1));
 uresult();
 
-goal LPomega_thy "|- Lam A:*.Lam P:A->A->*.Lam a:A.P^a^a : ?T";
+goal LPomega_thy "|- Lam A:*.Lam P:A->A->*.Lam a:A. P^a^a : ?T";
 by (DEPTH_SOLVE (ares_tac LPomega 1));
 uresult();
 
 (* CONSTRUCTIONS *)
 
-goal CC_thy "|- Lam A:*.Lam P:A->*.Lam a:A.P^a->Pi P:*.P: ?T";
+goal CC_thy "|- Lam A:*.Lam P:A->*.Lam a:A. P^a->Pi P:*.P: ?T";
 by (DEPTH_SOLVE (ares_tac CC 1));
 uresult();
 
-goal CC_thy "|- Lam A:*.Lam P:A->*.Pi a:A.P^a: ?T";
+goal CC_thy "|- Lam A:*.Lam P:A->*.Pi a:A. P^a: ?T";
 by (DEPTH_SOLVE (ares_tac CC 1));
 uresult();
 
-goal CC_thy "A:* P:A->* a:A |- ?p : (Pi a:A.P^a)->P^a";
+goal CC_thy "A:* P:A->* a:A |- ?p : (Pi a:A. P^a)->P^a";
 by (strip_asms_tac CC 1);
 by (rtac lam_ss 1);
 by (DEPTH_SOLVE_1(ares_tac CC 1));
@@ -208,7 +208,7 @@
 by (DEPTH_SOLVE(ares_tac LP2 1));
 uresult();
 
-goal CC_thy "Lam A:*.Lam c:A.Lam f:A->A. \
+goal CC_thy "Lam A:*.Lam c:A. Lam f:A->A. \
 \       Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";
 by (DEPTH_SOLVE(ares_tac CC 1));
 uresult();
@@ -219,7 +219,7 @@
 by (rtac lam_ss 1);
 by (DEPTH_SOLVE_1(ares_tac LP2 1));
 by (DEPTH_SOLVE_1(ares_tac LP2 2));
-by (eres_inst_tac [("a","Lam x:A.Pi Q:A->*.Q^x->Q^a")] pi_elim 1);
+by (eres_inst_tac [("a","Lam x:A. Pi Q:A->*.Q^x->Q^a")] pi_elim 1);
 by (DEPTH_SOLVE_1(ares_tac LP2 1));
 by (rewtac beta);
 by (etac imp_elim 1);
diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/FOLP.ML
--- a/src/FOLP/FOLP.ML	Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/FOLP.ML	Fri Oct 10 16:29:41 1997 +0200
@@ -27,7 +27,7 @@
 (*** Classical introduction rules for | and EX ***)
 
 val disjCI = prove_goal FOLP.thy 
-   "(!!x.x:~Q ==> f(x):P) ==> ?p : P|Q"
+   "(!!x. x:~Q ==> f(x):P) ==> ?p : P|Q"
  (fn prems=>
   [ (rtac classical 1),
     (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
@@ -35,14 +35,14 @@
 
 (*introduction rule involving only EX*)
 val ex_classical = prove_goal FOLP.thy 
-   "( !!u.u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x.P(x)"
+   "( !!u. u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x. P(x)"
  (fn prems=>
   [ (rtac classical 1),
     (eresolve_tac (prems RL [exI]) 1) ]);
 
 (*version of above, simplifying ~EX to ALL~ *)
 val exCI = prove_goal FOLP.thy 
-   "(!!u.u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x.P(x)"
+   "(!!u. u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x. P(x)"
  (fn [prem]=>
   [ (rtac ex_classical 1),
     (resolve_tac [notI RS allI RS prem] 1),
@@ -58,7 +58,7 @@
 
 (*Classical implies (-->) elimination. *)
 val impCE = prove_goal FOLP.thy 
-    "[| p:P-->Q;  !!x.x:~P ==> f(x):R;  !!y.y:Q ==> g(y):R |] ==> ?p : R"
+    "[| p:P-->Q;  !!x. x:~P ==> f(x):R;  !!y. y:Q ==> g(y):R |] ==> ?p : R"
  (fn major::prems=>
   [ (resolve_tac [excluded_middle RS disjE] 1),
     (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
@@ -84,7 +84,7 @@
 
 (*Should be used as swap since ~P becomes redundant*)
 val swap = prove_goal FOLP.thy 
-   "p:~P ==> (!!x.x:~Q ==> f(x):P) ==> ?p : Q"
+   "p:~P ==> (!!x. x:~Q ==> f(x):P) ==> ?p : Q"
  (fn major::prems=>
   [ (rtac classical 1),
     (rtac (major RS notE) 1),
diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/FOLP.thy
--- a/src/FOLP/FOLP.thy	Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/FOLP.thy	Fri Oct 10 16:29:41 1997 +0200
@@ -10,5 +10,5 @@
 consts
   cla :: "[p=>p]=>p"
 rules
-  classical "(!!x.x:~P ==> f(x):P) ==> cla(f):P"
+  classical "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
 end
diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/IFOLP.ML
--- a/src/FOLP/IFOLP.ML	Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/IFOLP.ML	Fri Oct 10 16:29:41 1997 +0200
@@ -82,23 +82,23 @@
               resolve_tac prems 1))) ]);
 
 val impE = prove_goal IFOLP.thy 
-    "[| p:P-->Q;  q:P;  !!x.x:Q ==> r(x):R |] ==> ?p:R"
+    "[| p:P-->Q;  q:P;  !!x. x:Q ==> r(x):R |] ==> ?p:R"
  (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
 
 val allE = prove_goal IFOLP.thy 
-    "[| p:ALL x.P(x); !!y.y:P(x) ==> q(y):R |] ==> ?p:R"
+    "[| p:ALL x. P(x); !!y. y:P(x) ==> q(y):R |] ==> ?p:R"
  (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
 
 (*Duplicates the quantifier; for use with eresolve_tac*)
 val all_dupE = prove_goal IFOLP.thy 
-    "[| p:ALL x.P(x);  !!y z.[| y:P(x); z:ALL x.P(x) |] ==> q(y,z):R \
+    "[| p:ALL x. P(x);  !!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R \
 \    |] ==> ?p:R"
  (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
 
 
 (*** Negation rules, which translate between ~P and P-->False ***)
 
-val notI = prove_goalw IFOLP.thy [not_def]  "(!!x.x:P ==> q(x):False) ==> ?p:~P"
+val notI = prove_goalw IFOLP.thy [not_def]  "(!!x. x:P ==> q(x):False) ==> ?p:~P"
  (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]);
 
 val notE = prove_goalw IFOLP.thy [not_def] "[| p:~P;  q:P |] ==> ?p:R"
@@ -108,7 +108,7 @@
 
 (*This is useful with the special implication rules for each kind of P. *)
 val not_to_imp = prove_goal IFOLP.thy 
-    "[| p:~P;  !!x.x:(P-->False) ==> q(x):Q |] ==> ?p:Q"
+    "[| p:~P;  !!x. x:(P-->False) ==> q(x):Q |] ==> ?p:Q"
  (fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]);
 
 
@@ -121,7 +121,7 @@
 
 
 (*Contrapositive of an inference rule*)
-val contrapos = prove_goal IFOLP.thy "[| p:~Q;  !!y.y:P==>q(y):Q |] ==> ?a:~P"
+val contrapos = prove_goal IFOLP.thy "[| p:~Q;  !!y. y:P==>q(y):Q |] ==> ?a:~P"
  (fn [major,minor]=> 
   [ (rtac (major RS notE RS notI) 1), 
     (etac minor 1) ]);
@@ -161,7 +161,7 @@
 (*** If-and-only-if ***)
 
 val iffI = prove_goalw IFOLP.thy [iff_def]
-   "[| !!x.x:P ==> q(x):Q;  !!x.x:Q ==> r(x):P |] ==> ?p:P<->Q"
+   "[| !!x. x:P ==> q(x):Q;  !!x. x:Q ==> r(x):P |] ==> ?p:P<->Q"
  (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]);
 
 
@@ -201,11 +201,11 @@
 ***)
 
 val ex1I = prove_goalw IFOLP.thy [ex1_def]
-    "[| p:P(a);  !!x u.u:P(x) ==> f(u) : x=a |] ==> ?p:EX! x. P(x)"
+    "[| p:P(a);  !!x u. u:P(x) ==> f(u) : x=a |] ==> ?p:EX! x. P(x)"
  (fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
 
 val ex1E = prove_goalw IFOLP.thy [ex1_def]
-    "[| p:EX! x.P(x);  \
+    "[| p:EX! x. P(x);  \
 \       !!x u v. [| u:P(x);  v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R |] ==>\
 \    ?a : R"
  (fn prems =>
@@ -221,7 +221,7 @@
     REPEAT1 (eresolve_tac [asm_rl,mp] i);
 
 val conj_cong = prove_goal IFOLP.thy 
-    "[| p:P <-> P';  !!x.x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')"
+    "[| p:P <-> P';  !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')"
  (fn prems =>
   [ (cut_facts_tac prems 1),
     (REPEAT  (ares_tac [iffI,conjI] 1
@@ -237,7 +237,7 @@
       ORELSE  mp_tac 1)) ]);
 
 val imp_cong = prove_goal IFOLP.thy 
-    "[| p:P <-> P';  !!x.x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')"
+    "[| p:P <-> P';  !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')"
  (fn prems =>
   [ (cut_facts_tac prems 1),
     (REPEAT   (ares_tac [iffI,impI] 1
@@ -261,14 +261,14 @@
       ORELSE  eresolve_tac [iffE,notE] 1)) ]);
 
 val all_cong = prove_goal IFOLP.thy 
-    "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(ALL x.P(x)) <-> (ALL x.Q(x))"
+    "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(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)) ]);
 
 val ex_cong = prove_goal IFOLP.thy 
-    "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX x.P(x)) <-> (EX x.Q(x))"
+    "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(EX x. P(x)) <-> (EX x. Q(x))"
  (fn prems =>
   [ (REPEAT   (etac exE 1 ORELSE ares_tac [iffI,exI] 1
       ORELSE   mp_tac 1
@@ -306,7 +306,7 @@
 
 (*A special case of ex1E that would otherwise need quantifier expansion*)
 val ex1_equalsE = prove_goal IFOLP.thy
-    "[| p:EX! x.P(x);  q:P(a);  r:P(b) |] ==> ?d:a=b"
+    "[| p:EX! x. P(x);  q:P(a);  r:P(b) |] ==> ?d:a=b"
  (fn prems =>
   [ (cut_facts_tac prems 1),
     (etac ex1E 1),
@@ -395,7 +395,7 @@
     (preprint, University of St Andrews, 1991)  ***)
 
 val conj_impE = prove_goal IFOLP.thy 
-    "[| p:(P&Q)-->S;  !!x.x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R"
+    "[| p:(P&Q)-->S;  !!x. x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R"
  (fn major::prems=>
   [ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]);
 
@@ -407,7 +407,7 @@
 (*Simplifies the implication.  Classical version is stronger. 
   Still UNSAFE since Q must be provable -- backtracking needed.  *)
 val imp_impE = prove_goal IFOLP.thy 
-    "[| p:(P-->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  !!x.x:S ==> r(x):R |] ==> \
+    "[| p:(P-->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  !!x. x:S ==> r(x):R |] ==> \
 \    ?p:R"
  (fn major::prems=>
   [ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]);
@@ -415,26 +415,26 @@
 (*Simplifies the implication.  Classical version is stronger. 
   Still UNSAFE since ~P must be provable -- backtracking needed.  *)
 val not_impE = prove_goal IFOLP.thy
-    "[| p:~P --> S;  !!y.y:P ==> q(y):False;  !!y.y:S ==> r(y):R |] ==> ?p:R"
+    "[| p:~P --> S;  !!y. y:P ==> q(y):False;  !!y. y:S ==> r(y):R |] ==> ?p:R"
  (fn major::prems=>
   [ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]);
 
 (*Simplifies the implication.   UNSAFE.  *)
 val iff_impE = prove_goal IFOLP.thy 
     "[| p:(P<->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  \
-\       !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P;  !!x.x:S ==> s(x):R |] ==> ?p:R"
+\       !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P;  !!x. x:S ==> s(x):R |] ==> ?p:R"
  (fn major::prems=>
   [ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]);
 
 (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
 val all_impE = prove_goal IFOLP.thy 
-    "[| p:(ALL x.P(x))-->S;  !!x.q:P(x);  !!y.y:S ==> r(y):R |] ==> ?p:R"
+    "[| p:(ALL x. P(x))-->S;  !!x. q:P(x);  !!y. y:S ==> r(y):R |] ==> ?p: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.  *)
 val ex_impE = prove_goal IFOLP.thy 
-    "[| p:(EX x.P(x))-->S;  !!y.y:P(a)-->S ==> q(y):R |] ==> ?p:R"
+    "[| p:(EX x. P(x))-->S;  !!y. y:P(a)-->S ==> q(y):R |] ==> ?p:R"
  (fn major::prems=>
   [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]);
 
diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/IFOLP.thy	Fri Oct 10 16:29:41 1997 +0200
@@ -67,7 +67,7 @@
 (* Like Intensional Equality in MLTT - but proofs distinct from terms *)
 
 ieqI      "ideq(a) : a=a"
-ieqE      "[| p : a=b;  !!x.f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
+ieqE      "[| p : a=b;  !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
 
 (* Truth and Falsity *)
 
@@ -84,21 +84,21 @@
 
 disjI1    "a:P ==> inl(a):P|Q"
 disjI2    "b:Q ==> inr(b):P|Q"
-disjE     "[| a:P|Q;  !!x.x:P ==> f(x):R;  !!x.x:Q ==> g(x):R 
+disjE     "[| a:P|Q;  !!x. x:P ==> f(x):R;  !!x. x:Q ==> g(x):R 
           |] ==> when(a,f,g):R"
 
 (* Implication *)
 
-impI      "(!!x.x:P ==> f(x):Q) ==> lam x.f(x):P-->Q"
+impI      "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
 mp        "[| f:P-->Q;  a:P |] ==> f`a:Q"
 
 (*Quantifiers*)
 
-allI      "(!!x. f(x) : P(x)) ==> all x.f(x) : ALL x.P(x)"
-spec      "(f:ALL x.P(x)) ==> f^x : P(x)"
+allI      "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
+spec      "(f:ALL x. P(x)) ==> f^x : P(x)"
 
-exI       "p : P(x) ==> [x,p] : EX x.P(x)"
-exE       "[| p: EX x.P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
+exI       "p : P(x) ==> [x,p] : EX x. P(x)"
+exE       "[| p: EX x. P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
 
 (**** Equality between proofs ****)
 
@@ -106,20 +106,20 @@
 psym      "a = b : P ==> b = a : P"
 ptrans    "[| a = b : P;  b = c : P |] ==> a = c : P"
 
-idpeelB   "[| !!x.f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
+idpeelB   "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
 
 fstB      "a:P ==> fst(<a,b>) = a : P"
 sndB      "b:Q ==> snd(<a,b>) = b : Q"
 pairEC    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
 
-whenBinl  "[| a:P;  !!x.x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
-whenBinr  "[| b:P;  !!x.x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
-plusEC    "a:P|Q ==> when(a,%x.inl(x),%y.inr(y)) = p : P|Q"
+whenBinl  "[| a:P;  !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
+whenBinr  "[| b:P;  !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
+plusEC    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = p : P|Q"
 
-applyB     "[| a:P;  !!x.x:P ==> b(x) : Q |] ==> (lam x.b(x)) ` a = b(a) : Q"
-funEC      "f:P ==> f = lam x.f`x : P"
+applyB     "[| a:P;  !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
+funEC      "f:P ==> f = lam x. f`x : P"
 
-specB      "[| !!x.f(x) : P(x) |] ==> (all x.f(x)) ^ a = f(a) : P(a)"
+specB      "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
 
 
 (**** Definitions ****)
diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/ROOT.ML
--- a/src/FOLP/ROOT.ML	Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ROOT.ML	Fri Oct 10 16:29:41 1997 +0200
@@ -33,7 +33,7 @@
 
   (*etac rev_cut_eq moves an equality to be the last premise. *)
   val rev_cut_eq = prove_goal IFOLP.thy 
-                "[| p:a=b;  !!x.x:a=b ==> f(x):R |] ==> ?p:R"
+                "[| p:a=b;  !!x. x:a=b ==> f(x):R |] ==> ?p:R"
    (fn prems => [ REPEAT(resolve_tac prems 1) ]);
 
   val rev_mp = rev_mp
diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/ex/If.ML
--- a/src/FOLP/ex/If.ML	Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ex/If.ML	Fri Oct 10 16:29:41 1997 +0200
@@ -10,7 +10,7 @@
 open Cla;    (*in case structure Int is open!*)
 
 val prems = goalw If.thy [if_def]
-    "[| !!x.x:P ==> f(x):Q; !!x.x:~P ==> g(x):R |] ==> ?p:if(P,Q,R)";
+    "[| !!x. x:P ==> f(x):Q; !!x. x:~P ==> g(x):R |] ==> ?p:if(P,Q,R)";
 by (fast_tac (FOLP_cs addIs prems) 1);
 val ifI = result();
 
diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/ex/cla.ML
--- a/src/FOLP/ex/cla.ML	Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ex/cla.ML	Fri Oct 10 16:29:41 1997 +0200
@@ -127,15 +127,15 @@
 by (fast_tac FOLP_cs 1);
 result(); 
 
-goal FOLP.thy "?p : (EX x. P-->Q(x))  <->  (P --> (EX x.Q(x)))";
+goal FOLP.thy "?p : (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
 by (fast_tac FOLP_cs 1);
 result(); 
 
-goal FOLP.thy "?p : (EX x.P(x)-->Q)  <->  (ALL x.P(x)) --> Q";
+goal FOLP.thy "?p : (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
 by (fast_tac FOLP_cs 1);
 result(); 
 
-goal FOLP.thy "?p : (ALL x.P(x)) | Q  <->  (ALL x. P(x) | Q)";
+goal FOLP.thy "?p : (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
 by (fast_tac FOLP_cs 1);
 result(); 
 
@@ -192,7 +192,7 @@
 
 writeln"Problem 24";
 goal FOLP.thy "?p : ~(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 (fast_tac FOLP_cs 1); 
 result();
@@ -225,7 +225,7 @@
 writeln"Problem 28.  AMENDED";
 goal FOLP.thy "?p : (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 (fast_tac FOLP_cs 1);  
 result();
@@ -245,7 +245,7 @@
 result();
 
 writeln"Problem 31";
-goal FOLP.thy "?p : ~(EX x.P(x) & (Q(x) | R(x))) & \
+goal FOLP.thy "?p : ~(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))";
@@ -282,7 +282,7 @@
 
 writeln"Problem 37";
 goal FOLP.thy "?p : (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))";
@@ -323,7 +323,7 @@
 
 writeln"Problem 50";  
 (*What has this to do with equality?*)
-goal FOLP.thy "?p : (ALL x. P(a,x) | (ALL y.P(x,y))) --> (EX x. ALL y.P(x,y))";
+goal FOLP.thy "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
 by (best_tac FOLP_dup_cs 1);
 result();
 
diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/ex/foundn.ML
--- a/src/FOLP/ex/foundn.ML	Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ex/foundn.ML	Fri Oct 10 16:29:41 1997 +0200
@@ -99,7 +99,7 @@
 
 
 (*Parallel lifting example. *)
-goal IFOLP.thy "?p : EX u.ALL x.EX v.ALL y.EX w. P(u,x,v,y,w)";
+goal IFOLP.thy "?p : 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 IFOLP.thy "p : (EX z.F(z)) & B ==> ?p:(EX z. F(z) & B)";
+goal IFOLP.thy "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
 by (rtac conjE 1);
 by (resolve_tac prems 1);
 by (rtac exE 1);
diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/ex/int.ML
--- a/src/FOLP/ex/int.ML	Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ex/int.ML	Fri Oct 10 16:29:41 1997 +0200
@@ -180,11 +180,11 @@
 
 writeln"The converse is classical in the following implications...";
 
-goal IFOLP.thy "?p : (EX x.P(x)-->Q)  -->  (ALL x.P(x)) --> Q";
+goal IFOLP.thy "?p : (EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q";
 by (IntPr.fast_tac 1); 
 result();  
 
-goal IFOLP.thy "?p : ((ALL x.P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
+goal IFOLP.thy "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
 by (IntPr.fast_tac 1); 
 result();  
 
@@ -192,7 +192,7 @@
 by (IntPr.fast_tac 1); 
 result();  
 
-goal IFOLP.thy "?p : (ALL x.P(x)) | Q  -->  (ALL x. P(x) | Q)";
+goal IFOLP.thy "?p : (ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)";
 by (IntPr.fast_tac 1); 
 result();  
 
@@ -206,15 +206,15 @@
 writeln"The following are not constructively valid!";
 (*The attempt to prove them terminates quickly!*)
 
-goal IFOLP.thy "?p : ((ALL x.P(x))-->Q) --> (EX x.P(x)-->Q)";
+goal IFOLP.thy "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)";
 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
 getgoal 1; 
 
-goal IFOLP.thy "?p : (P --> (EX x.Q(x))) --> (EX x. P-->Q(x))";
+goal IFOLP.thy "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))";
 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
 getgoal 1; 
 
-goal IFOLP.thy "?p : (ALL x. P(x) | Q) --> ((ALL x.P(x)) | Q)";
+goal IFOLP.thy "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)";
 by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
 getgoal 1; 
 
@@ -264,7 +264,7 @@
 
 writeln"Problem 24";
 goal IFOLP.thy "?p : ~(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; 
@@ -297,7 +297,7 @@
 result();
 
 writeln"Problem 31";
-goal IFOLP.thy "?p : ~(EX x.P(x) & (Q(x) | R(x))) & \
+goal IFOLP.thy "?p : ~(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))";
diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/ex/intro.ML
--- a/src/FOLP/ex/intro.ML	Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ex/intro.ML	Fri Oct 10 16:29:41 1997 +0200
@@ -32,7 +32,7 @@
 result();
 
 (*Correct version, delaying use of "spec" until last*)
-goal FOLP.thy "?p:(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
+goal FOLP.thy "?p:(ALL x y. P(x,y))  -->  (ALL z w. P(w,z))";
 by (rtac impI 1);
 by (rtac allI 1);
 by (rtac allI 1);
@@ -69,7 +69,7 @@
 
 (** Derivation of negation introduction **)
 
-val prems = goal FOLP.thy "(!!x.x:P ==> f(x):False) ==> ?p:~P";
+val prems = goal FOLP.thy "(!!x. x:P ==> f(x):False) ==> ?p:~P";
 by (rewtac not_def);
 by (rtac impI 1);
 by (resolve_tac prems 1);
diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/ex/quant.ML
--- a/src/FOLP/ex/quant.ML	Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ex/quant.ML	Fri Oct 10 16:29:41 1997 +0200
@@ -9,40 +9,40 @@
 
 writeln"File FOLP/ex/quant.ML";
 
-goal thy "?p : (ALL x y.P(x,y))  -->  (ALL y x.P(x,y))";
+goal thy "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))";
 by tac;
 result();  
 
 
-goal thy "?p : (EX x y.P(x,y)) --> (EX y x.P(x,y))";
+goal thy "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))";
 by tac;
 result();  
 
 
 (*Converse is false*)
-goal thy "?p : (ALL x.P(x)) | (ALL x.Q(x)) --> (ALL x. P(x) | Q(x))";
+goal thy "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
 by tac;
 result();  
 
-goal thy "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x.Q(x)))";
+goal thy "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))";
 by tac;
 result();  
 
 
-goal thy "?p : (ALL x.P(x)-->Q)  <->  ((EX x.P(x)) --> Q)";
+goal thy "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
 by tac;
 result();  
 
 
 writeln"Some harder ones";
 
-goal thy "?p : (EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))";
+goal thy "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
 by tac;
 result();  
 (*6 secs*)
 
 (*Converse is false*)
-goal thy "?p : (EX x. P(x)&Q(x)) --> (EX x.P(x))  &  (EX x.Q(x))";
+goal thy "?p : (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 : P(?a) --> (ALL x.P(x))";
+goal thy "?p : 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 : (P(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))";
+    "?p : (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 "?p : (ALL x.P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))";
+goal thy "?p : (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 : (P --> (EX x.Q(x))) & P --> (EX x.Q(x))";
+goal thy "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
 by tac;  
 result();  
 
diff -r 9a5a4e123859 -r f1a1817659e6 src/FOLP/simpdata.ML
--- a/src/FOLP/simpdata.ML	Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/simpdata.ML	Fri Oct 10 16:29:41 1997 +0200
@@ -41,17 +41,17 @@
   "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
 
 val quant_rews = 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_rews  = map int_prove_fun
  ["~(P|Q) <-> ~P & ~Q",
   "P & (Q | R) <-> P&Q | P&R", "(Q | R) & P <-> Q&P | R&P",
   "(P | Q --> R) <-> (P --> R) & (Q --> R)",
-  "~(EX x.NORM(P(x))) <-> (ALL x. ~NORM(P(x)))",
-  "((EX x.NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)",
-  "(EX x.NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))",
-  "NORM(Q) & (EX x.NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"];
+  "~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))",
+  "((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)",
+  "(EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))",
+  "NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"];
 
 val P_Imp_P_iff_T = int_prove_fun_raw "p:P ==> ?p:(P <-> True)";