src/HOL/UNITY/UNITY_tactics.ML
changeset 45138 ba618e9288b8
parent 42795 66fcc9882784
child 46752 e9e7209eb375
equal deleted inserted replaced
45137:6e422d180de8 45138:ba618e9288b8
    44       res_inst_tac ctxt
    44       res_inst_tac ctxt
    45         [(("act", 0), sact)] @{thm totalize_transientI} 2
    45         [(("act", 0), sact)] @{thm totalize_transientI} 2
    46       ORELSE res_inst_tac ctxt
    46       ORELSE res_inst_tac ctxt
    47         [(("act", 0), sact)] @{thm transientI} 2,
    47         [(("act", 0), sact)] @{thm transientI} 2,
    48          (*simplify the command's domain*)
    48          (*simplify the command's domain*)
    49       simp_tac (simpset_of ctxt addsimps [@{thm Domain_def}]) 3,
    49       simp_tac (simpset_of ctxt addsimps @{thms Domain_def}) 3,
    50       constrains_tac ctxt 1,
    50       constrains_tac ctxt 1,
    51       ALLGOALS (clarify_tac ctxt),
    51       ALLGOALS (clarify_tac ctxt),
    52       ALLGOALS (asm_lr_simp_tac (simpset_of ctxt))]);
    52       ALLGOALS (asm_lr_simp_tac (simpset_of ctxt))]);
    53 
    53 
    54 
    54