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