equal
deleted
inserted
replaced
284 apply blast |
284 apply blast |
285 apply (blast) (* asm *) |
285 apply (blast) (* asm *) |
286 apply (blast) (* cut *) |
286 apply (blast) (* cut *) |
287 apply (blast) (* weaken *) |
287 apply (blast) (* weaken *) |
288 apply (tactic {* ALLGOALS (EVERY' |
288 apply (tactic {* ALLGOALS (EVERY' |
289 [REPEAT o thin_tac @{context} "hoare_derivs ?x ?y", |
289 [REPEAT o Rule_Insts.thin_tac @{context} "hoare_derivs ?x ?y", |
290 simp_tac @{context}, clarify_tac @{context}, REPEAT o smp_tac @{context} 1]) *}) |
290 simp_tac @{context}, clarify_tac @{context}, REPEAT o smp_tac @{context} 1]) *}) |
291 apply (simp_all (no_asm_use) add: triple_valid_def2) |
291 apply (simp_all (no_asm_use) add: triple_valid_def2) |
292 apply (intro strip, tactic "smp_tac @{context} 2 1", blast) (* conseq *) |
292 apply (intro strip, tactic "smp_tac @{context} 2 1", blast) (* conseq *) |
293 apply (tactic {* ALLGOALS (clarsimp_tac @{context}) *}) (* Skip, Ass, Local *) |
293 apply (tactic {* ALLGOALS (clarsimp_tac @{context}) *}) (* Skip, Ass, Local *) |
294 prefer 3 apply (force) (* Call *) |
294 prefer 3 apply (force) (* Call *) |