equal
deleted
inserted
replaced
272 fun simproc ctxt redex = |
272 fun simproc ctxt redex = |
273 let |
273 let |
274 val t = HOLogic.mk_Trueprop (Thm.term_of redex); |
274 val t = HOLogic.mk_Trueprop (Thm.term_of redex); |
275 fun tac {context = ctxt, prems = _ } = |
275 fun tac {context = ctxt, prems = _ } = |
276 SOLVE (measurable_tac ctxt (Simplifier.prems_of ctxt)); |
276 SOLVE (measurable_tac ctxt (Simplifier.prems_of ctxt)); |
277 in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end; |
277 in \<^try>\<open>Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}\<close> end; |
278 |
278 |
279 end |
279 end |
280 |
280 |