src/HOL/Tools/Meson/meson.ML
changeset 52230 1105b3b5aa77
parent 51717 9e7d1c139569
child 54742 7a86358a3c0b
equal deleted inserted replaced
52228:ee8e3eaad24c 52230:1105b3b5aa77
   552    @{const_name Let}]
   552    @{const_name Let}]
   553 
   553 
   554 fun presimplify ctxt =
   554 fun presimplify ctxt =
   555   rewrite_rule (map safe_mk_meta_eq nnf_simps)
   555   rewrite_rule (map safe_mk_meta_eq nnf_simps)
   556   #> simplify (put_simpset nnf_ss ctxt)
   556   #> simplify (put_simpset nnf_ss ctxt)
   557   #> Raw_Simplifier.rewrite_rule @{thms Let_def [abs_def]}
   557   #> rewrite_rule @{thms Let_def [abs_def]}
   558 
   558 
   559 fun make_nnf ctxt th = case prems_of th of
   559 fun make_nnf ctxt th = case prems_of th of
   560     [] => th |> presimplify ctxt |> make_nnf1 ctxt
   560     [] => th |> presimplify ctxt |> make_nnf1 ctxt
   561   | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
   561   | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
   562 
   562