src/FOL/ex/mini.ML

                    "~(ALL x.P(x)) <-> (EX x. ~P(x))",
                    "~(EX x.P(x)) <-> (ALL x. ~P(x))"];
 
 (*** Removal of --> and <-> (positive and negative occurrences) ***)
 (*Last one is important for computing a compact CNF*)
-val nnf_rews = map prove_fun
+val nnf_simps = map prove_fun
                 ["(P-->Q) <-> (~P | Q)",
                  "~(P-->Q) <-> (P & ~Q)",
                  "(P<->Q) <-> (~P | Q) & (~Q | P)",
                  "~(P<->Q) <-> (P | Q) & (~P | ~Q)"];
 
 (* BEWARE: rewrite rules for <-> can confuse the simplifier!! *)
 
 (*** Pushing in the existential quantifiers ***)
 
-val ex_rews = map prove_fun 
+val ex_simps = map prove_fun 
                 ["(EX x. P) <-> P",
                  "(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(x)) <-> (EX x.P(x)) | (EX x.Q(x))",
                  "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q",
                  "(EX x. P | Q(x)) <-> P | (EX x.Q(x))"];
 
 (*** Pushing in the universal quantifiers ***)
 
-val all_rews = map prove_fun
+val all_simps = map prove_fun
                 ["(ALL x. P) <-> P",
                  "(ALL x. P(x) & Q(x)) <-> (ALL x.P(x)) & (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",

   setmksimps (map mk_meta_eq o atomize o gen_all)
   setsolver  (fn prems => resolve_tac (triv_rls@prems) 
                           ORELSE' assume_tac
                           ORELSE' etac FalseE)
   setsubgoaler asm_simp_tac
-  addsimps (demorgans @ nnf_rews @ ex_rews @ all_rews);
+  addsimps (demorgans @ nnf_simps @ ex_simps @ all_simps);
 
 val mini_tac = rtac ccontr THEN' asm_full_simp_tac mini_ss;