--- a/src/HOL/Tools/meson.ML Wed Jul 05 16:24:10 2006 +0200
+++ b/src/HOL/Tools/meson.ML Wed Jul 05 16:24:28 2006 +0200
@@ -279,7 +279,7 @@
incomplete, since when actually called, the only connectives likely to
remain are & | Not.*)
val is_conn = member (op =)
- ["Trueprop", "HOL.tag", "op &", "op |", "op -->", "op =", "Not",
+ ["Trueprop", "op &", "op |", "op -->", "op =", "Not",
"All", "Ex", "Ball", "Bex"];
(*True if the term contains a function where the type of any argument contains
@@ -386,13 +386,11 @@
(tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
handle THM _ => th;
-(*The simplification removes defined quantifiers and occurrences of True and False,
- as well as tags applied to True and False. nnf_ss also includes the one-point simprocs,
+(*The simplification removes defined quantifiers and occurrences of True and False.
+ nnf_ss also includes the one-point simprocs,
which are needed to avoid the various one-point theorems from generating junk clauses.*)
-val tag_True = thm "tag_True";
-val tag_False = thm "tag_False";
val nnf_simps =
- [simp_implies_def, Ex1_def, Ball_def, Bex_def, tag_True, tag_False, if_True,
+ [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True,
if_False, if_cancel, if_eq_cancel, cases_simp];
val nnf_extra_simps =
thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;