equal
deleted
inserted
replaced
280 apply blast |
280 apply blast |
281 apply blast |
281 apply blast |
282 apply (blast) (* asm *) |
282 apply (blast) (* asm *) |
283 apply (blast) (* cut *) |
283 apply (blast) (* cut *) |
284 apply (blast) (* weaken *) |
284 apply (blast) (* weaken *) |
285 apply (tactic {* ALLGOALS (EVERY'[REPEAT o thin_tac "hoare_derivs ?x ?y", SIMPSET' simp_tac, CLASET' clarify_tac, REPEAT o smp_tac 1]) *}) |
285 apply (tactic {* ALLGOALS (EVERY' |
|
286 [REPEAT o RuleInsts.thin_tac @{context} "hoare_derivs ?x ?y", |
|
287 simp_tac @{simpset}, clarify_tac @{claset}, REPEAT o smp_tac 1]) *}) |
286 apply (simp_all (no_asm_use) add: triple_valid_def2) |
288 apply (simp_all (no_asm_use) add: triple_valid_def2) |
287 apply (intro strip, tactic "smp_tac 2 1", blast) (* conseq *) |
289 apply (intro strip, tactic "smp_tac 2 1", blast) (* conseq *) |
288 apply (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *}) (* Skip, Ass, Local *) |
290 apply (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *}) (* Skip, Ass, Local *) |
289 prefer 3 apply (force) (* Call *) |
291 prefer 3 apply (force) (* Call *) |
290 apply (erule_tac [2] evaln_elim_cases) (* If *) |
292 apply (erule_tac [2] evaln_elim_cases) (* If *) |