--- a/src/HOL/Tools/meson.ML Mon May 09 16:40:11 2005 +0200
+++ b/src/HOL/Tools/meson.ML Mon May 09 16:40:37 2005 +0200
@@ -311,8 +311,8 @@
(tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
handle THM _ => th;
-(*The simplification removes occurrences of True and False.*)
-val nnf_ss = HOL_basic_ss addsimps Ball_def::Bex_def::simp_thms;
+(*The simplification removes defined quantifiers and occurrences of True and False.*)
+val nnf_ss = HOL_basic_ss addsimps Ex1_def::Ball_def::Bex_def::simp_thms;
fun make_nnf th = th |> simplify nnf_ss
|> check_no_bool |> make_nnf1