equal
deleted
inserted
replaced
651 \<close> |
651 \<close> |
652 |
652 |
653 end |
653 end |
654 |
654 |
655 setup \<open> |
655 setup \<open> |
656 map_theory_simpset (fn ctxt0 => ctxt0 addSolver |
656 map_theory_simpset (fn ctxt0 => ctxt0 |> Simplifier.add_unsafe_solver |
657 mk_solver "partial and linear orders" (fn ctxt => HOL_Order_Tac.tac (Simplifier.prems_of ctxt) ctxt)) |
657 (mk_solver "partial and linear orders" (fn ctxt => HOL_Order_Tac.tac (Simplifier.prems_of ctxt) ctxt))) |
658 \<close> |
658 \<close> |
659 |
659 |
660 ML \<open> |
660 ML \<open> |
661 local |
661 local |
662 fun prp t thm = Thm.prop_of thm = t; (* FIXME proper aconv!? *) |
662 fun prp t thm = Thm.prop_of thm = t; (* FIXME proper aconv!? *) |