src/FOL/IFOL.ML

 qed_goal "impE" IFOL.thy 
     "[| P-->Q;  P;  Q ==> R |] ==> R"
  (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)) ]);
 
 
 (*** Negation rules, which translate between ~P and P-->False ***)

     "[| P(a);  !!x. P(x) ==> x=a |] ==> EX! x. P(x)"
  (fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
 
 (*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)) ]);
 
 

     (REPEAT   (ares_tac [iffI,notI] 1
       ORELSE  mp_tac 1
       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
       ORELSE   iff_tac prems 1)) ]);
 

 bind_thm ("ssubst", sym RS subst);
 fun stac th = CHANGED o rtac (th RS ssubst);
 
 (*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),
     (rtac trans 1),
     (rtac sym 2),

  (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*)
 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)) ]);
 
 (*** Courtesy of Krzysztof Grabczewski ***)