src/HOL/Decision_Procs/langford.ML
changeset 55847 c38ad094e5bf
parent 55846 b56fda32bf24
child 55848 1bfe72d14630
equal deleted inserted replaced
55846:b56fda32bf24 55847:c38ad094e5bf
   178 
   178 
   179 end;
   179 end;
   180 
   180 
   181 fun raw_dlo_conv ctxt dlo_ss ({qe_bnds, qe_nolb, qe_noub, gst, gs, ...}: Langford_Data.entry) =
   181 fun raw_dlo_conv ctxt dlo_ss ({qe_bnds, qe_nolb, qe_noub, gst, gs, ...}: Langford_Data.entry) =
   182   let
   182   let
   183     val ctxt' = put_simpset dlo_ss ctxt addsimps @{thms dnf_simps} addsimprocs [reduce_ex_simproc]
   183     val ctxt' =
       
   184       Context_Position.set_visible false (put_simpset dlo_ss ctxt)
       
   185         addsimps @{thms dnf_simps} addsimprocs [reduce_ex_simproc]
   184     val dnfex_conv = Simplifier.rewrite ctxt'
   186     val dnfex_conv = Simplifier.rewrite ctxt'
   185     val pcv =
   187     val pcv =
   186       Simplifier.rewrite
   188       Simplifier.rewrite
   187         (put_simpset dlo_ss ctxt
   189         (put_simpset dlo_ss ctxt
   188           addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
   190           addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})