fixed dots;
authorwenzelm
Fri Oct 10 16:29:41 1997 +0200 (1997-10-10)
changeset 3836f1a1817659e6
parent 3835 9a5a4e123859
child 3837 d7f033c74b38
fixed dots;
src/Cube/ex/ex.ML
src/FOLP/FOLP.ML
src/FOLP/FOLP.thy
src/FOLP/IFOLP.ML
src/FOLP/IFOLP.thy
src/FOLP/ROOT.ML
src/FOLP/ex/If.ML
src/FOLP/ex/cla.ML
src/FOLP/ex/foundn.ML
src/FOLP/ex/int.ML
src/FOLP/ex/intro.ML
src/FOLP/ex/quant.ML
src/FOLP/simpdata.ML
     1.1 --- a/src/Cube/ex/ex.ML	Fri Oct 10 15:52:12 1997 +0200
     1.2 +++ b/src/Cube/ex/ex.ML	Fri Oct 10 16:29:41 1997 +0200
     1.3 @@ -19,37 +19,37 @@
     1.4  by (DEPTH_SOLVE (ares_tac simple 1));
     1.5  uresult();
     1.6  
     1.7 -goal thy "A:* |- Lam a:A.a : ?T";
     1.8 +goal thy "A:* |- Lam a:A. a : ?T";
     1.9  by (DEPTH_SOLVE (ares_tac simple 1));
    1.10  uresult();
    1.11  
    1.12 -goal thy "A:* B:* b:B |- Lam x:A.b : ?T";
    1.13 +goal thy "A:* B:* b:B |- Lam x:A. b : ?T";
    1.14  by (DEPTH_SOLVE (ares_tac simple 1));
    1.15  uresult();
    1.16  
    1.17 -goal thy "A:* b:A |- (Lam a:A.a)^b: ?T";
    1.18 +goal thy "A:* b:A |- (Lam a:A. a)^b: ?T";
    1.19  by (DEPTH_SOLVE (ares_tac simple 1));
    1.20  uresult();
    1.21  
    1.22 -goal thy "A:* B:* c:A b:B |- (Lam x:A.b)^ c: ?T";
    1.23 +goal thy "A:* B:* c:A b:B |- (Lam x:A. b)^ c: ?T";
    1.24  by (DEPTH_SOLVE (ares_tac simple 1));
    1.25  uresult();
    1.26  
    1.27 -goal thy "A:* B:* |- Lam a:A.Lam b:B.a : ?T";
    1.28 +goal thy "A:* B:* |- Lam a:A. Lam b:B. a : ?T";
    1.29  by (DEPTH_SOLVE (ares_tac simple 1));
    1.30  uresult();
    1.31  
    1.32  (* SECOND-ORDER TYPES *)
    1.33  
    1.34 -goal L2_thy "|- Lam A:*. Lam a:A.a : ?T";
    1.35 +goal L2_thy "|- Lam A:*. Lam a:A. a : ?T";
    1.36  by (DEPTH_SOLVE (ares_tac L2 1));
    1.37  uresult();
    1.38  
    1.39 -goal L2_thy "A:* |- (Lam B:*.Lam b:B.b)^A : ?T";
    1.40 +goal L2_thy "A:* |- (Lam B:*.Lam b:B. b)^A : ?T";
    1.41  by (DEPTH_SOLVE (ares_tac L2 1));
    1.42  uresult();
    1.43  
    1.44 -goal L2_thy "A:* b:A |- (Lam B:*.Lam b:B.b) ^ A ^ b: ?T";
    1.45 +goal L2_thy "A:* b:A |- (Lam B:*.Lam b:B. b) ^ A ^ b: ?T";
    1.46  by (DEPTH_SOLVE (ares_tac L2 1));
    1.47  uresult();
    1.48  
    1.49 @@ -67,7 +67,7 @@
    1.50  by (DEPTH_SOLVE (ares_tac Lomega 1));
    1.51  uresult();
    1.52  
    1.53 -goal Lomega_thy "B:* b:B |- (Lam y:B.b): ?T";
    1.54 +goal Lomega_thy "B:* b:B |- (Lam y:B. b): ?T";
    1.55  by (DEPTH_SOLVE (ares_tac Lomega 1));
    1.56  uresult();
    1.57  
    1.58 @@ -89,28 +89,28 @@
    1.59  by (DEPTH_SOLVE (ares_tac LP 1));
    1.60  uresult();
    1.61  
    1.62 -goal LP_thy "A:* P:A->A->* a:A |- Pi a:A.P^a^a: ?T";
    1.63 +goal LP_thy "A:* P:A->A->* a:A |- Pi a:A. P^a^a: ?T";
    1.64  by (DEPTH_SOLVE (ares_tac LP 1));
    1.65  uresult();
    1.66  
    1.67 -goal LP_thy "A:* P:A->* Q:A->* |- Pi a:A.P^a -> Q^a: ?T";
    1.68 +goal LP_thy "A:* P:A->* Q:A->* |- Pi a:A. P^a -> Q^a: ?T";
    1.69  by (DEPTH_SOLVE (ares_tac LP 1));
    1.70  uresult();
    1.71  
    1.72 -goal LP_thy "A:* P:A->* |- Pi a:A.P^a -> P^a: ?T";
    1.73 +goal LP_thy "A:* P:A->* |- Pi a:A. P^a -> P^a: ?T";
    1.74  by (DEPTH_SOLVE (ares_tac LP 1));
    1.75  uresult();
    1.76  
    1.77 -goal LP_thy "A:* P:A->* |- Lam a:A.Lam x:P^a.x: ?T";
    1.78 +goal LP_thy "A:* P:A->* |- Lam a:A. Lam x:P^a. x: ?T";
    1.79  by (DEPTH_SOLVE (ares_tac LP 1));
    1.80  uresult();
    1.81  
    1.82 -goal LP_thy "A:* P:A->* Q:* |- (Pi a:A.P^a->Q) -> (Pi a:A.P^a) -> Q : ?T";
    1.83 +goal LP_thy "A:* P:A->* Q:* |- (Pi a:A. P^a->Q) -> (Pi a:A. P^a) -> Q : ?T";
    1.84  by (DEPTH_SOLVE (ares_tac LP 1));
    1.85  uresult();
    1.86  
    1.87  goal LP_thy "A:* P:A->* Q:* a0:A |- \
    1.88 -\       Lam x:Pi a:A.P^a->Q. Lam y:Pi a:A.P^a. x^a0^(y^a0): ?T";
    1.89 +\       Lam x:Pi a:A. P^a->Q. Lam y:Pi a:A. P^a. x^a0^(y^a0): ?T";
    1.90  by (DEPTH_SOLVE (ares_tac LP 1));
    1.91  uresult();
    1.92  
    1.93 @@ -124,7 +124,7 @@
    1.94  by (DEPTH_SOLVE (ares_tac LOmega 1));
    1.95  uresult();
    1.96  
    1.97 -goal LOmega_thy "|- Lam A:*.Lam B:*.Lam x:A.Lam y:B.x : ?T";
    1.98 +goal LOmega_thy "|- Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T";
    1.99  by (DEPTH_SOLVE (ares_tac LOmega 1));
   1.100  uresult();
   1.101  
   1.102 @@ -148,18 +148,18 @@
   1.103  
   1.104  (* Second-order Predicate Logic *)
   1.105  
   1.106 -goal LP2_thy "A:* P:A->* |- Lam a:A.P^a->(Pi A:*.A) : ?T";
   1.107 +goal LP2_thy "A:* P:A->* |- Lam a:A. P^a->(Pi A:*.A) : ?T";
   1.108  by (DEPTH_SOLVE (ares_tac LP2 1));
   1.109  uresult();
   1.110  
   1.111  goal LP2_thy "A:* P:A->A->* |- \
   1.112 -\       (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";
   1.113 +\       (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";
   1.114  by (DEPTH_SOLVE (ares_tac LP2 1));
   1.115  uresult();
   1.116  
   1.117  (* Antisymmetry implies irreflexivity: *)
   1.118  goal LP2_thy "A:* P:A->A->* |- \
   1.119 -\       ?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";
   1.120 +\       ?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";
   1.121  by (strip_asms_tac LP2 1);
   1.122  by (rtac lam_ss 1);
   1.123  by (DEPTH_SOLVE_1(ares_tac LP2 1));
   1.124 @@ -175,25 +175,25 @@
   1.125  
   1.126  (* LPomega *)
   1.127  
   1.128 -goal LPomega_thy "A:* |- Lam P:A->A->*.Lam a:A.P^a^a : ?T";
   1.129 +goal LPomega_thy "A:* |- Lam P:A->A->*.Lam a:A. P^a^a : ?T";
   1.130  by (DEPTH_SOLVE (ares_tac LPomega 1));
   1.131  uresult();
   1.132  
   1.133 -goal LPomega_thy "|- Lam A:*.Lam P:A->A->*.Lam a:A.P^a^a : ?T";
   1.134 +goal LPomega_thy "|- Lam A:*.Lam P:A->A->*.Lam a:A. P^a^a : ?T";
   1.135  by (DEPTH_SOLVE (ares_tac LPomega 1));
   1.136  uresult();
   1.137  
   1.138  (* CONSTRUCTIONS *)
   1.139  
   1.140 -goal CC_thy "|- Lam A:*.Lam P:A->*.Lam a:A.P^a->Pi P:*.P: ?T";
   1.141 +goal CC_thy "|- Lam A:*.Lam P:A->*.Lam a:A. P^a->Pi P:*.P: ?T";
   1.142  by (DEPTH_SOLVE (ares_tac CC 1));
   1.143  uresult();
   1.144  
   1.145 -goal CC_thy "|- Lam A:*.Lam P:A->*.Pi a:A.P^a: ?T";
   1.146 +goal CC_thy "|- Lam A:*.Lam P:A->*.Pi a:A. P^a: ?T";
   1.147  by (DEPTH_SOLVE (ares_tac CC 1));
   1.148  uresult();
   1.149  
   1.150 -goal CC_thy "A:* P:A->* a:A |- ?p : (Pi a:A.P^a)->P^a";
   1.151 +goal CC_thy "A:* P:A->* a:A |- ?p : (Pi a:A. P^a)->P^a";
   1.152  by (strip_asms_tac CC 1);
   1.153  by (rtac lam_ss 1);
   1.154  by (DEPTH_SOLVE_1(ares_tac CC 1));
   1.155 @@ -208,7 +208,7 @@
   1.156  by (DEPTH_SOLVE(ares_tac LP2 1));
   1.157  uresult();
   1.158  
   1.159 -goal CC_thy "Lam A:*.Lam c:A.Lam f:A->A. \
   1.160 +goal CC_thy "Lam A:*.Lam c:A. Lam f:A->A. \
   1.161  \       Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";
   1.162  by (DEPTH_SOLVE(ares_tac CC 1));
   1.163  uresult();
   1.164 @@ -219,7 +219,7 @@
   1.165  by (rtac lam_ss 1);
   1.166  by (DEPTH_SOLVE_1(ares_tac LP2 1));
   1.167  by (DEPTH_SOLVE_1(ares_tac LP2 2));
   1.168 -by (eres_inst_tac [("a","Lam x:A.Pi Q:A->*.Q^x->Q^a")] pi_elim 1);
   1.169 +by (eres_inst_tac [("a","Lam x:A. Pi Q:A->*.Q^x->Q^a")] pi_elim 1);
   1.170  by (DEPTH_SOLVE_1(ares_tac LP2 1));
   1.171  by (rewtac beta);
   1.172  by (etac imp_elim 1);
     2.1 --- a/src/FOLP/FOLP.ML	Fri Oct 10 15:52:12 1997 +0200
     2.2 +++ b/src/FOLP/FOLP.ML	Fri Oct 10 16:29:41 1997 +0200
     2.3 @@ -27,7 +27,7 @@
     2.4  (*** Classical introduction rules for | and EX ***)
     2.5  
     2.6  val disjCI = prove_goal FOLP.thy 
     2.7 -   "(!!x.x:~Q ==> f(x):P) ==> ?p : P|Q"
     2.8 +   "(!!x. x:~Q ==> f(x):P) ==> ?p : P|Q"
     2.9   (fn prems=>
    2.10    [ (rtac classical 1),
    2.11      (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
    2.12 @@ -35,14 +35,14 @@
    2.13  
    2.14  (*introduction rule involving only EX*)
    2.15  val ex_classical = prove_goal FOLP.thy 
    2.16 -   "( !!u.u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x.P(x)"
    2.17 +   "( !!u. u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x. P(x)"
    2.18   (fn prems=>
    2.19    [ (rtac classical 1),
    2.20      (eresolve_tac (prems RL [exI]) 1) ]);
    2.21  
    2.22  (*version of above, simplifying ~EX to ALL~ *)
    2.23  val exCI = prove_goal FOLP.thy 
    2.24 -   "(!!u.u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x.P(x)"
    2.25 +   "(!!u. u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x. P(x)"
    2.26   (fn [prem]=>
    2.27    [ (rtac ex_classical 1),
    2.28      (resolve_tac [notI RS allI RS prem] 1),
    2.29 @@ -58,7 +58,7 @@
    2.30  
    2.31  (*Classical implies (-->) elimination. *)
    2.32  val impCE = prove_goal FOLP.thy 
    2.33 -    "[| p:P-->Q;  !!x.x:~P ==> f(x):R;  !!y.y:Q ==> g(y):R |] ==> ?p : R"
    2.34 +    "[| p:P-->Q;  !!x. x:~P ==> f(x):R;  !!y. y:Q ==> g(y):R |] ==> ?p : R"
    2.35   (fn major::prems=>
    2.36    [ (resolve_tac [excluded_middle RS disjE] 1),
    2.37      (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
    2.38 @@ -84,7 +84,7 @@
    2.39  
    2.40  (*Should be used as swap since ~P becomes redundant*)
    2.41  val swap = prove_goal FOLP.thy 
    2.42 -   "p:~P ==> (!!x.x:~Q ==> f(x):P) ==> ?p : Q"
    2.43 +   "p:~P ==> (!!x. x:~Q ==> f(x):P) ==> ?p : Q"
    2.44   (fn major::prems=>
    2.45    [ (rtac classical 1),
    2.46      (rtac (major RS notE) 1),
     3.1 --- a/src/FOLP/FOLP.thy	Fri Oct 10 15:52:12 1997 +0200
     3.2 +++ b/src/FOLP/FOLP.thy	Fri Oct 10 16:29:41 1997 +0200
     3.3 @@ -10,5 +10,5 @@
     3.4  consts
     3.5    cla :: "[p=>p]=>p"
     3.6  rules
     3.7 -  classical "(!!x.x:~P ==> f(x):P) ==> cla(f):P"
     3.8 +  classical "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
     3.9  end
     4.1 --- a/src/FOLP/IFOLP.ML	Fri Oct 10 15:52:12 1997 +0200
     4.2 +++ b/src/FOLP/IFOLP.ML	Fri Oct 10 16:29:41 1997 +0200
     4.3 @@ -82,23 +82,23 @@
     4.4                resolve_tac prems 1))) ]);
     4.5  
     4.6  val impE = prove_goal IFOLP.thy 
     4.7 -    "[| p:P-->Q;  q:P;  !!x.x:Q ==> r(x):R |] ==> ?p:R"
     4.8 +    "[| p:P-->Q;  q:P;  !!x. x:Q ==> r(x):R |] ==> ?p:R"
     4.9   (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
    4.10  
    4.11  val allE = prove_goal IFOLP.thy 
    4.12 -    "[| p:ALL x.P(x); !!y.y:P(x) ==> q(y):R |] ==> ?p:R"
    4.13 +    "[| p:ALL x. P(x); !!y. y:P(x) ==> q(y):R |] ==> ?p:R"
    4.14   (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
    4.15  
    4.16  (*Duplicates the quantifier; for use with eresolve_tac*)
    4.17  val all_dupE = prove_goal IFOLP.thy 
    4.18 -    "[| p:ALL x.P(x);  !!y z.[| y:P(x); z:ALL x.P(x) |] ==> q(y,z):R \
    4.19 +    "[| p:ALL x. P(x);  !!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R \
    4.20  \    |] ==> ?p:R"
    4.21   (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
    4.22  
    4.23  
    4.24  (*** Negation rules, which translate between ~P and P-->False ***)
    4.25  
    4.26 -val notI = prove_goalw IFOLP.thy [not_def]  "(!!x.x:P ==> q(x):False) ==> ?p:~P"
    4.27 +val notI = prove_goalw IFOLP.thy [not_def]  "(!!x. x:P ==> q(x):False) ==> ?p:~P"
    4.28   (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]);
    4.29  
    4.30  val notE = prove_goalw IFOLP.thy [not_def] "[| p:~P;  q:P |] ==> ?p:R"
    4.31 @@ -108,7 +108,7 @@
    4.32  
    4.33  (*This is useful with the special implication rules for each kind of P. *)
    4.34  val not_to_imp = prove_goal IFOLP.thy 
    4.35 -    "[| p:~P;  !!x.x:(P-->False) ==> q(x):Q |] ==> ?p:Q"
    4.36 +    "[| p:~P;  !!x. x:(P-->False) ==> q(x):Q |] ==> ?p:Q"
    4.37   (fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]);
    4.38  
    4.39  
    4.40 @@ -121,7 +121,7 @@
    4.41  
    4.42  
    4.43  (*Contrapositive of an inference rule*)
    4.44 -val contrapos = prove_goal IFOLP.thy "[| p:~Q;  !!y.y:P==>q(y):Q |] ==> ?a:~P"
    4.45 +val contrapos = prove_goal IFOLP.thy "[| p:~Q;  !!y. y:P==>q(y):Q |] ==> ?a:~P"
    4.46   (fn [major,minor]=> 
    4.47    [ (rtac (major RS notE RS notI) 1), 
    4.48      (etac minor 1) ]);
    4.49 @@ -161,7 +161,7 @@
    4.50  (*** If-and-only-if ***)
    4.51  
    4.52  val iffI = prove_goalw IFOLP.thy [iff_def]
    4.53 -   "[| !!x.x:P ==> q(x):Q;  !!x.x:Q ==> r(x):P |] ==> ?p:P<->Q"
    4.54 +   "[| !!x. x:P ==> q(x):Q;  !!x. x:Q ==> r(x):P |] ==> ?p:P<->Q"
    4.55   (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]);
    4.56  
    4.57  
    4.58 @@ -201,11 +201,11 @@
    4.59  ***)
    4.60  
    4.61  val ex1I = prove_goalw IFOLP.thy [ex1_def]
    4.62 -    "[| p:P(a);  !!x u.u:P(x) ==> f(u) : x=a |] ==> ?p:EX! x. P(x)"
    4.63 +    "[| p:P(a);  !!x u. u:P(x) ==> f(u) : x=a |] ==> ?p:EX! x. P(x)"
    4.64   (fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
    4.65  
    4.66  val ex1E = prove_goalw IFOLP.thy [ex1_def]
    4.67 -    "[| p:EX! x.P(x);  \
    4.68 +    "[| p:EX! x. P(x);  \
    4.69  \       !!x u v. [| u:P(x);  v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R |] ==>\
    4.70  \    ?a : R"
    4.71   (fn prems =>
    4.72 @@ -221,7 +221,7 @@
    4.73      REPEAT1 (eresolve_tac [asm_rl,mp] i);
    4.74  
    4.75  val conj_cong = prove_goal IFOLP.thy 
    4.76 -    "[| p:P <-> P';  !!x.x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')"
    4.77 +    "[| p:P <-> P';  !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')"
    4.78   (fn prems =>
    4.79    [ (cut_facts_tac prems 1),
    4.80      (REPEAT  (ares_tac [iffI,conjI] 1
    4.81 @@ -237,7 +237,7 @@
    4.82        ORELSE  mp_tac 1)) ]);
    4.83  
    4.84  val imp_cong = prove_goal IFOLP.thy 
    4.85 -    "[| p:P <-> P';  !!x.x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')"
    4.86 +    "[| p:P <-> P';  !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')"
    4.87   (fn prems =>
    4.88    [ (cut_facts_tac prems 1),
    4.89      (REPEAT   (ares_tac [iffI,impI] 1
    4.90 @@ -261,14 +261,14 @@
    4.91        ORELSE  eresolve_tac [iffE,notE] 1)) ]);
    4.92  
    4.93  val all_cong = prove_goal IFOLP.thy 
    4.94 -    "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(ALL x.P(x)) <-> (ALL x.Q(x))"
    4.95 +    "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
    4.96   (fn prems =>
    4.97    [ (REPEAT   (ares_tac [iffI,allI] 1
    4.98        ORELSE   mp_tac 1
    4.99        ORELSE   etac allE 1 ORELSE iff_tac prems 1)) ]);
   4.100  
   4.101  val ex_cong = prove_goal IFOLP.thy 
   4.102 -    "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX x.P(x)) <-> (EX x.Q(x))"
   4.103 +    "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(EX x. P(x)) <-> (EX x. Q(x))"
   4.104   (fn prems =>
   4.105    [ (REPEAT   (etac exE 1 ORELSE ares_tac [iffI,exI] 1
   4.106        ORELSE   mp_tac 1
   4.107 @@ -306,7 +306,7 @@
   4.108  
   4.109  (*A special case of ex1E that would otherwise need quantifier expansion*)
   4.110  val ex1_equalsE = prove_goal IFOLP.thy
   4.111 -    "[| p:EX! x.P(x);  q:P(a);  r:P(b) |] ==> ?d:a=b"
   4.112 +    "[| p:EX! x. P(x);  q:P(a);  r:P(b) |] ==> ?d:a=b"
   4.113   (fn prems =>
   4.114    [ (cut_facts_tac prems 1),
   4.115      (etac ex1E 1),
   4.116 @@ -395,7 +395,7 @@
   4.117      (preprint, University of St Andrews, 1991)  ***)
   4.118  
   4.119  val conj_impE = prove_goal IFOLP.thy 
   4.120 -    "[| p:(P&Q)-->S;  !!x.x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R"
   4.121 +    "[| p:(P&Q)-->S;  !!x. x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R"
   4.122   (fn major::prems=>
   4.123    [ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]);
   4.124  
   4.125 @@ -407,7 +407,7 @@
   4.126  (*Simplifies the implication.  Classical version is stronger. 
   4.127    Still UNSAFE since Q must be provable -- backtracking needed.  *)
   4.128  val imp_impE = prove_goal IFOLP.thy 
   4.129 -    "[| p:(P-->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  !!x.x:S ==> r(x):R |] ==> \
   4.130 +    "[| p:(P-->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  !!x. x:S ==> r(x):R |] ==> \
   4.131  \    ?p:R"
   4.132   (fn major::prems=>
   4.133    [ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]);
   4.134 @@ -415,26 +415,26 @@
   4.135  (*Simplifies the implication.  Classical version is stronger. 
   4.136    Still UNSAFE since ~P must be provable -- backtracking needed.  *)
   4.137  val not_impE = prove_goal IFOLP.thy
   4.138 -    "[| p:~P --> S;  !!y.y:P ==> q(y):False;  !!y.y:S ==> r(y):R |] ==> ?p:R"
   4.139 +    "[| p:~P --> S;  !!y. y:P ==> q(y):False;  !!y. y:S ==> r(y):R |] ==> ?p:R"
   4.140   (fn major::prems=>
   4.141    [ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]);
   4.142  
   4.143  (*Simplifies the implication.   UNSAFE.  *)
   4.144  val iff_impE = prove_goal IFOLP.thy 
   4.145      "[| p:(P<->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  \
   4.146 -\       !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P;  !!x.x:S ==> s(x):R |] ==> ?p:R"
   4.147 +\       !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P;  !!x. x:S ==> s(x):R |] ==> ?p:R"
   4.148   (fn major::prems=>
   4.149    [ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]);
   4.150  
   4.151  (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
   4.152  val all_impE = prove_goal IFOLP.thy 
   4.153 -    "[| p:(ALL x.P(x))-->S;  !!x.q:P(x);  !!y.y:S ==> r(y):R |] ==> ?p:R"
   4.154 +    "[| p:(ALL x. P(x))-->S;  !!x. q:P(x);  !!y. y:S ==> r(y):R |] ==> ?p:R"
   4.155   (fn major::prems=>
   4.156    [ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]);
   4.157  
   4.158  (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
   4.159  val ex_impE = prove_goal IFOLP.thy 
   4.160 -    "[| p:(EX x.P(x))-->S;  !!y.y:P(a)-->S ==> q(y):R |] ==> ?p:R"
   4.161 +    "[| p:(EX x. P(x))-->S;  !!y. y:P(a)-->S ==> q(y):R |] ==> ?p:R"
   4.162   (fn major::prems=>
   4.163    [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]);
   4.164  
     5.1 --- a/src/FOLP/IFOLP.thy	Fri Oct 10 15:52:12 1997 +0200
     5.2 +++ b/src/FOLP/IFOLP.thy	Fri Oct 10 16:29:41 1997 +0200
     5.3 @@ -67,7 +67,7 @@
     5.4  (* Like Intensional Equality in MLTT - but proofs distinct from terms *)
     5.5  
     5.6  ieqI      "ideq(a) : a=a"
     5.7 -ieqE      "[| p : a=b;  !!x.f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
     5.8 +ieqE      "[| p : a=b;  !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
     5.9  
    5.10  (* Truth and Falsity *)
    5.11  
    5.12 @@ -84,21 +84,21 @@
    5.13  
    5.14  disjI1    "a:P ==> inl(a):P|Q"
    5.15  disjI2    "b:Q ==> inr(b):P|Q"
    5.16 -disjE     "[| a:P|Q;  !!x.x:P ==> f(x):R;  !!x.x:Q ==> g(x):R 
    5.17 +disjE     "[| a:P|Q;  !!x. x:P ==> f(x):R;  !!x. x:Q ==> g(x):R 
    5.18            |] ==> when(a,f,g):R"
    5.19  
    5.20  (* Implication *)
    5.21  
    5.22 -impI      "(!!x.x:P ==> f(x):Q) ==> lam x.f(x):P-->Q"
    5.23 +impI      "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
    5.24  mp        "[| f:P-->Q;  a:P |] ==> f`a:Q"
    5.25  
    5.26  (*Quantifiers*)
    5.27  
    5.28 -allI      "(!!x. f(x) : P(x)) ==> all x.f(x) : ALL x.P(x)"
    5.29 -spec      "(f:ALL x.P(x)) ==> f^x : P(x)"
    5.30 +allI      "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
    5.31 +spec      "(f:ALL x. P(x)) ==> f^x : P(x)"
    5.32  
    5.33 -exI       "p : P(x) ==> [x,p] : EX x.P(x)"
    5.34 -exE       "[| p: EX x.P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
    5.35 +exI       "p : P(x) ==> [x,p] : EX x. P(x)"
    5.36 +exE       "[| p: EX x. P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
    5.37  
    5.38  (**** Equality between proofs ****)
    5.39  
    5.40 @@ -106,20 +106,20 @@
    5.41  psym      "a = b : P ==> b = a : P"
    5.42  ptrans    "[| a = b : P;  b = c : P |] ==> a = c : P"
    5.43  
    5.44 -idpeelB   "[| !!x.f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
    5.45 +idpeelB   "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
    5.46  
    5.47  fstB      "a:P ==> fst(<a,b>) = a : P"
    5.48  sndB      "b:Q ==> snd(<a,b>) = b : Q"
    5.49  pairEC    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
    5.50  
    5.51 -whenBinl  "[| a:P;  !!x.x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
    5.52 -whenBinr  "[| b:P;  !!x.x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
    5.53 -plusEC    "a:P|Q ==> when(a,%x.inl(x),%y.inr(y)) = p : P|Q"
    5.54 +whenBinl  "[| a:P;  !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
    5.55 +whenBinr  "[| b:P;  !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
    5.56 +plusEC    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = p : P|Q"
    5.57  
    5.58 -applyB     "[| a:P;  !!x.x:P ==> b(x) : Q |] ==> (lam x.b(x)) ` a = b(a) : Q"
    5.59 -funEC      "f:P ==> f = lam x.f`x : P"
    5.60 +applyB     "[| a:P;  !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
    5.61 +funEC      "f:P ==> f = lam x. f`x : P"
    5.62  
    5.63 -specB      "[| !!x.f(x) : P(x) |] ==> (all x.f(x)) ^ a = f(a) : P(a)"
    5.64 +specB      "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
    5.65  
    5.66  
    5.67  (**** Definitions ****)
     6.1 --- a/src/FOLP/ROOT.ML	Fri Oct 10 15:52:12 1997 +0200
     6.2 +++ b/src/FOLP/ROOT.ML	Fri Oct 10 16:29:41 1997 +0200
     6.3 @@ -33,7 +33,7 @@
     6.4  
     6.5    (*etac rev_cut_eq moves an equality to be the last premise. *)
     6.6    val rev_cut_eq = prove_goal IFOLP.thy 
     6.7 -                "[| p:a=b;  !!x.x:a=b ==> f(x):R |] ==> ?p:R"
     6.8 +                "[| p:a=b;  !!x. x:a=b ==> f(x):R |] ==> ?p:R"
     6.9     (fn prems => [ REPEAT(resolve_tac prems 1) ]);
    6.10  
    6.11    val rev_mp = rev_mp
     7.1 --- a/src/FOLP/ex/If.ML	Fri Oct 10 15:52:12 1997 +0200
     7.2 +++ b/src/FOLP/ex/If.ML	Fri Oct 10 16:29:41 1997 +0200
     7.3 @@ -10,7 +10,7 @@
     7.4  open Cla;    (*in case structure Int is open!*)
     7.5  
     7.6  val prems = goalw If.thy [if_def]
     7.7 -    "[| !!x.x:P ==> f(x):Q; !!x.x:~P ==> g(x):R |] ==> ?p:if(P,Q,R)";
     7.8 +    "[| !!x. x:P ==> f(x):Q; !!x. x:~P ==> g(x):R |] ==> ?p:if(P,Q,R)";
     7.9  by (fast_tac (FOLP_cs addIs prems) 1);
    7.10  val ifI = result();
    7.11  
     8.1 --- a/src/FOLP/ex/cla.ML	Fri Oct 10 15:52:12 1997 +0200
     8.2 +++ b/src/FOLP/ex/cla.ML	Fri Oct 10 16:29:41 1997 +0200
     8.3 @@ -127,15 +127,15 @@
     8.4  by (fast_tac FOLP_cs 1);
     8.5  result(); 
     8.6  
     8.7 -goal FOLP.thy "?p : (EX x. P-->Q(x))  <->  (P --> (EX x.Q(x)))";
     8.8 +goal FOLP.thy "?p : (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
     8.9  by (fast_tac FOLP_cs 1);
    8.10  result(); 
    8.11  
    8.12 -goal FOLP.thy "?p : (EX x.P(x)-->Q)  <->  (ALL x.P(x)) --> Q";
    8.13 +goal FOLP.thy "?p : (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
    8.14  by (fast_tac FOLP_cs 1);
    8.15  result(); 
    8.16  
    8.17 -goal FOLP.thy "?p : (ALL x.P(x)) | Q  <->  (ALL x. P(x) | Q)";
    8.18 +goal FOLP.thy "?p : (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
    8.19  by (fast_tac FOLP_cs 1);
    8.20  result(); 
    8.21  
    8.22 @@ -192,7 +192,7 @@
    8.23  
    8.24  writeln"Problem 24";
    8.25  goal FOLP.thy "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
    8.26 -\    (~(EX x.P(x)) --> (EX x.Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
    8.27 +\    (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
    8.28  \   --> (EX x. P(x)&R(x))";
    8.29  by (fast_tac FOLP_cs 1); 
    8.30  result();
    8.31 @@ -225,7 +225,7 @@
    8.32  writeln"Problem 28.  AMENDED";
    8.33  goal FOLP.thy "?p : (ALL x. P(x) --> (ALL x. Q(x))) &   \
    8.34  \       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
    8.35 -\       ((EX x.S(x)) --> (ALL x. L(x) --> M(x)))  \
    8.36 +\       ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))  \
    8.37  \   --> (ALL x. P(x) & L(x) --> M(x))";
    8.38  by (fast_tac FOLP_cs 1);  
    8.39  result();
    8.40 @@ -245,7 +245,7 @@
    8.41  result();
    8.42  
    8.43  writeln"Problem 31";
    8.44 -goal FOLP.thy "?p : ~(EX x.P(x) & (Q(x) | R(x))) & \
    8.45 +goal FOLP.thy "?p : ~(EX x. P(x) & (Q(x) | R(x))) & \
    8.46  \       (EX x. L(x) & P(x)) & \
    8.47  \       (ALL x. ~ R(x) --> M(x))  \
    8.48  \   --> (EX x. L(x) & M(x))";
    8.49 @@ -282,7 +282,7 @@
    8.50  
    8.51  writeln"Problem 37";
    8.52  goal FOLP.thy "?p : (ALL z. EX w. ALL x. EX y. \
    8.53 -\          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) & \
    8.54 +\          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \
    8.55  \       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
    8.56  \       ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
    8.57  \   --> (ALL x. EX y. R(x,y))";
    8.58 @@ -323,7 +323,7 @@
    8.59  
    8.60  writeln"Problem 50";  
    8.61  (*What has this to do with equality?*)
    8.62 -goal FOLP.thy "?p : (ALL x. P(a,x) | (ALL y.P(x,y))) --> (EX x. ALL y.P(x,y))";
    8.63 +goal FOLP.thy "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
    8.64  by (best_tac FOLP_dup_cs 1);
    8.65  result();
    8.66  
     9.1 --- a/src/FOLP/ex/foundn.ML	Fri Oct 10 15:52:12 1997 +0200
     9.2 +++ b/src/FOLP/ex/foundn.ML	Fri Oct 10 16:29:41 1997 +0200
     9.3 @@ -99,7 +99,7 @@
     9.4  
     9.5  
     9.6  (*Parallel lifting example. *)
     9.7 -goal IFOLP.thy "?p : EX u.ALL x.EX v.ALL y.EX w. P(u,x,v,y,w)";
     9.8 +goal IFOLP.thy "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
     9.9  by (resolve_tac [exI, allI] 1);
    9.10  by (resolve_tac [exI, allI] 1);
    9.11  by (resolve_tac [exI, allI] 1);
    9.12 @@ -108,7 +108,7 @@
    9.13  
    9.14  
    9.15  val prems =
    9.16 -goal IFOLP.thy "p : (EX z.F(z)) & B ==> ?p:(EX z. F(z) & B)";
    9.17 +goal IFOLP.thy "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
    9.18  by (rtac conjE 1);
    9.19  by (resolve_tac prems 1);
    9.20  by (rtac exE 1);
    10.1 --- a/src/FOLP/ex/int.ML	Fri Oct 10 15:52:12 1997 +0200
    10.2 +++ b/src/FOLP/ex/int.ML	Fri Oct 10 16:29:41 1997 +0200
    10.3 @@ -180,11 +180,11 @@
    10.4  
    10.5  writeln"The converse is classical in the following implications...";
    10.6  
    10.7 -goal IFOLP.thy "?p : (EX x.P(x)-->Q)  -->  (ALL x.P(x)) --> Q";
    10.8 +goal IFOLP.thy "?p : (EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q";
    10.9  by (IntPr.fast_tac 1); 
   10.10  result();  
   10.11  
   10.12 -goal IFOLP.thy "?p : ((ALL x.P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
   10.13 +goal IFOLP.thy "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
   10.14  by (IntPr.fast_tac 1); 
   10.15  result();  
   10.16  
   10.17 @@ -192,7 +192,7 @@
   10.18  by (IntPr.fast_tac 1); 
   10.19  result();  
   10.20  
   10.21 -goal IFOLP.thy "?p : (ALL x.P(x)) | Q  -->  (ALL x. P(x) | Q)";
   10.22 +goal IFOLP.thy "?p : (ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)";
   10.23  by (IntPr.fast_tac 1); 
   10.24  result();  
   10.25  
   10.26 @@ -206,15 +206,15 @@
   10.27  writeln"The following are not constructively valid!";
   10.28  (*The attempt to prove them terminates quickly!*)
   10.29  
   10.30 -goal IFOLP.thy "?p : ((ALL x.P(x))-->Q) --> (EX x.P(x)-->Q)";
   10.31 +goal IFOLP.thy "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)";
   10.32  by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   10.33  getgoal 1; 
   10.34  
   10.35 -goal IFOLP.thy "?p : (P --> (EX x.Q(x))) --> (EX x. P-->Q(x))";
   10.36 +goal IFOLP.thy "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))";
   10.37  by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   10.38  getgoal 1; 
   10.39  
   10.40 -goal IFOLP.thy "?p : (ALL x. P(x) | Q) --> ((ALL x.P(x)) | Q)";
   10.41 +goal IFOLP.thy "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)";
   10.42  by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   10.43  getgoal 1; 
   10.44  
   10.45 @@ -264,7 +264,7 @@
   10.46  
   10.47  writeln"Problem 24";
   10.48  goal IFOLP.thy "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
   10.49 -\    (~(EX x.P(x)) --> (EX x.Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
   10.50 +\    (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
   10.51  \   --> ~~(EX x. P(x)&R(x))";
   10.52  (*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
   10.53  by IntPr.safe_tac; 
   10.54 @@ -297,7 +297,7 @@
   10.55  result();
   10.56  
   10.57  writeln"Problem 31";
   10.58 -goal IFOLP.thy "?p : ~(EX x.P(x) & (Q(x) | R(x))) & \
   10.59 +goal IFOLP.thy "?p : ~(EX x. P(x) & (Q(x) | R(x))) & \
   10.60  \       (EX x. L(x) & P(x)) & \
   10.61  \       (ALL x. ~ R(x) --> M(x))  \
   10.62  \   --> (EX x. L(x) & M(x))";
    11.1 --- a/src/FOLP/ex/intro.ML	Fri Oct 10 15:52:12 1997 +0200
    11.2 +++ b/src/FOLP/ex/intro.ML	Fri Oct 10 16:29:41 1997 +0200
    11.3 @@ -32,7 +32,7 @@
    11.4  result();
    11.5  
    11.6  (*Correct version, delaying use of "spec" until last*)
    11.7 -goal FOLP.thy "?p:(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
    11.8 +goal FOLP.thy "?p:(ALL x y. P(x,y))  -->  (ALL z w. P(w,z))";
    11.9  by (rtac impI 1);
   11.10  by (rtac allI 1);
   11.11  by (rtac allI 1);
   11.12 @@ -69,7 +69,7 @@
   11.13  
   11.14  (** Derivation of negation introduction **)
   11.15  
   11.16 -val prems = goal FOLP.thy "(!!x.x:P ==> f(x):False) ==> ?p:~P";
   11.17 +val prems = goal FOLP.thy "(!!x. x:P ==> f(x):False) ==> ?p:~P";
   11.18  by (rewtac not_def);
   11.19  by (rtac impI 1);
   11.20  by (resolve_tac prems 1);
    12.1 --- a/src/FOLP/ex/quant.ML	Fri Oct 10 15:52:12 1997 +0200
    12.2 +++ b/src/FOLP/ex/quant.ML	Fri Oct 10 16:29:41 1997 +0200
    12.3 @@ -9,40 +9,40 @@
    12.4  
    12.5  writeln"File FOLP/ex/quant.ML";
    12.6  
    12.7 -goal thy "?p : (ALL x y.P(x,y))  -->  (ALL y x.P(x,y))";
    12.8 +goal thy "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))";
    12.9  by tac;
   12.10  result();  
   12.11  
   12.12  
   12.13 -goal thy "?p : (EX x y.P(x,y)) --> (EX y x.P(x,y))";
   12.14 +goal thy "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))";
   12.15  by tac;
   12.16  result();  
   12.17  
   12.18  
   12.19  (*Converse is false*)
   12.20 -goal thy "?p : (ALL x.P(x)) | (ALL x.Q(x)) --> (ALL x. P(x) | Q(x))";
   12.21 +goal thy "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
   12.22  by tac;
   12.23  result();  
   12.24  
   12.25 -goal thy "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x.Q(x)))";
   12.26 +goal thy "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))";
   12.27  by tac;
   12.28  result();  
   12.29  
   12.30  
   12.31 -goal thy "?p : (ALL x.P(x)-->Q)  <->  ((EX x.P(x)) --> Q)";
   12.32 +goal thy "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
   12.33  by tac;
   12.34  result();  
   12.35  
   12.36  
   12.37  writeln"Some harder ones";
   12.38  
   12.39 -goal thy "?p : (EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))";
   12.40 +goal thy "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
   12.41  by tac;
   12.42  result();  
   12.43  (*6 secs*)
   12.44  
   12.45  (*Converse is false*)
   12.46 -goal thy "?p : (EX x. P(x)&Q(x)) --> (EX x.P(x))  &  (EX x.Q(x))";
   12.47 +goal thy "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))";
   12.48  by tac;
   12.49  result();  
   12.50  
   12.51 @@ -70,26 +70,26 @@
   12.52  by tac handle ERROR => writeln"Failed, as expected";  
   12.53  getgoal 1; 
   12.54  
   12.55 -goal thy "?p : P(?a) --> (ALL x.P(x))";
   12.56 +goal thy "?p : P(?a) --> (ALL x. P(x))";
   12.57  by tac handle ERROR => writeln"Failed, as expected";
   12.58  (*Check that subgoals remain: proof failed.*)
   12.59  getgoal 1;  
   12.60  
   12.61  goal thy
   12.62 -    "?p : (P(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))";
   12.63 +    "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
   12.64  by tac handle ERROR => writeln"Failed, as expected";
   12.65  getgoal 1;  
   12.66  
   12.67  
   12.68  writeln"Back to things that are provable...";
   12.69  
   12.70 -goal thy "?p : (ALL x.P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))";
   12.71 +goal thy "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
   12.72  by tac;  
   12.73  result();  
   12.74  
   12.75  
   12.76  (*An example of why exI should be delayed as long as possible*)
   12.77 -goal thy "?p : (P --> (EX x.Q(x))) & P --> (EX x.Q(x))";
   12.78 +goal thy "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
   12.79  by tac;  
   12.80  result();  
   12.81  
    13.1 --- a/src/FOLP/simpdata.ML	Fri Oct 10 15:52:12 1997 +0200
    13.2 +++ b/src/FOLP/simpdata.ML	Fri Oct 10 16:29:41 1997 +0200
    13.3 @@ -41,17 +41,17 @@
    13.4    "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
    13.5  
    13.6  val quant_rews = map int_prove_fun
    13.7 - ["(ALL x.P) <-> P",    "(EX x.P) <-> P"];
    13.8 + ["(ALL x. P) <-> P",    "(EX x. P) <-> P"];
    13.9  
   13.10  (*These are NOT supplied by default!*)
   13.11  val distrib_rews  = map int_prove_fun
   13.12   ["~(P|Q) <-> ~P & ~Q",
   13.13    "P & (Q | R) <-> P&Q | P&R", "(Q | R) & P <-> Q&P | R&P",
   13.14    "(P | Q --> R) <-> (P --> R) & (Q --> R)",
   13.15 -  "~(EX x.NORM(P(x))) <-> (ALL x. ~NORM(P(x)))",
   13.16 -  "((EX x.NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)",
   13.17 -  "(EX x.NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))",
   13.18 -  "NORM(Q) & (EX x.NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"];
   13.19 +  "~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))",
   13.20 +  "((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)",
   13.21 +  "(EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))",
   13.22 +  "NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"];
   13.23  
   13.24  val P_Imp_P_iff_T = int_prove_fun_raw "p:P ==> ?p:(P <-> True)";
   13.25