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)";