src/FOL/simpdata.ML

  ["(True <-> P) <-> P",         "(P <-> True) <-> P",
   "(P <-> P) <-> True",
   "(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
  ["P & (Q | R) <-> P&Q | P&R", 
   "(Q | R) & P <-> Q&P | R&P",

 
 (*Miniscoping: pushing in existential quantifiers*)
 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), 
                    (IntPr.fast_tac 1) ]);
 

 int_prove "de_Morgan_disj" "(~(P | Q)) <-> (~P & ~Q)";
 prove     "de_Morgan_conj" "(~(P & Q)) <-> (~P | ~Q)";
 
 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"
     "(EX x. P(x) | Q(x)) <-> ((EX x. P(x)) | (EX x. Q(x)))";
 int_prove "all_conj_distrib"