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