equal
deleted
inserted
replaced
19 Args.goal_spec -- Scan.lift Args.name_source >> |
19 Args.goal_spec -- Scan.lift Args.name_source >> |
20 (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s)) |
20 (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s)) |
21 *} "for proving progress properties" |
21 *} "for proving progress properties" |
22 |
22 |
23 setup {* |
23 setup {* |
24 Simplifier.map_simpset_global (fn ss => ss |
24 map_theory_simpset (fn ctxt => ctxt |
25 addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair}) |
25 addsimps (make_o_equivs ctxt @{thm fst_o_funPair} @ make_o_equivs ctxt @{thm snd_o_funPair}) |
26 addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map})) |
26 addsimps (make_o_equivs ctxt @{thm fst_o_lift_map} @ make_o_equivs ctxt @{thm snd_o_lift_map})) |
27 *} |
27 *} |
28 |
28 |
29 end |
29 end |