equal
deleted
inserted
replaced
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 |