# HG changeset patch
# User paulson
# Date 841940934 -7200
# Node ID 4b5b2d04782ce42532100e8d85a0d6c4b5f7b17f
# Parent  832ccc1dba950fbbf81a1ae2ef35f1e813dc9a15
Some renaming.  Note that this miniscoping is more
general than that of ../simpdata.ML, as distributive laws are included.
On this other hand this version is for NNF only.

diff -r 832ccc1dba95 -r 4b5b2d04782c src/FOL/ex/mini.ML
--- a/src/FOL/ex/mini.ML	Thu Sep 05 18:28:01 1996 +0200
+++ b/src/FOL/ex/mini.ML	Thu Sep 05 18:28:54 1996 +0200
@@ -31,7 +31,7 @@
 
 (*** 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)",
@@ -41,7 +41,7 @@
 
 (*** 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))",
@@ -51,7 +51,7 @@
 
 (*** 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",
@@ -67,7 +67,7 @@
                           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;