src/HOL/Decision_Procs/ferrante_rackoff.ML
changeset 45654 cf10bde35973
parent 43333 2bdec7f430d3
child 46497 89ccf66aa73d
     1.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sun Nov 27 23:06:59 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sun Nov 27 23:10:19 2011 +0100
     1.3 @@ -163,7 +163,7 @@
     1.4                          qe))
     1.5                    [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
     1.6      val bex_conv =
     1.7 -      Simplifier.rewrite (HOL_basic_ss addsimps simp_thms@(@{thms "bex_simps" (1-5)}))
     1.8 +      Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms bex_simps(1-5)})
     1.9      val result_th = fconv_rule (arg_conv bex_conv) (Thm.transitive enth qe_th)
    1.10     in result_th
    1.11     end
    1.12 @@ -200,8 +200,8 @@
    1.13   let
    1.14     val ss = simpset
    1.15     val ss' =
    1.16 -     merge_ss (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps)
    1.17 -              @ [not_all,@{thm "all_not_ex"}, ex_disj_distrib], ss)
    1.18 +     merge_ss (HOL_basic_ss addsimps @{thms simp_thms ex_simps all_simps
    1.19 +                not_all all_not_ex ex_disj_distrib}, ss)
    1.20       |> Simplifier.inherit_context ss
    1.21     val pcv = Simplifier.rewrite ss'     
    1.22     val postcv = Simplifier.rewrite ss