src/HOL/Tools/meson.ML
changeset 37539 c80e77e8d036
parent 37410 2bf7e6136047
child 37781 2fbbf0a48cef
     1.1 --- a/src/HOL/Tools/meson.ML	Thu Jun 24 10:38:01 2010 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Thu Jun 24 17:25:47 2010 +0200
     1.3 @@ -521,10 +521,9 @@
     1.4    nnf_ss also includes the one-point simprocs,
     1.5    which are needed to avoid the various one-point theorems from generating junk clauses.*)
     1.6  val nnf_simps =
     1.7 -  [@{thm simp_implies_def}, @{thm Ex1_def}, @{thm Ball_def},@{thm  Bex_def}, @{thm if_True},
     1.8 -    @{thm if_False}, @{thm if_cancel}, @{thm if_eq_cancel}, @{thm cases_simp}];
     1.9 -val nnf_extra_simps =
    1.10 -  @{thms split_ifs} @ @{thms ex_simps} @ @{thms all_simps} @ @{thms simp_thms};
    1.11 +  @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel
    1.12 +         if_eq_cancel cases_simp}
    1.13 +val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
    1.14  
    1.15  val nnf_ss =
    1.16    HOL_basic_ss addsimps nnf_extra_simps