src/HOL/IMPP/Hoare.thy
changeset 59763 56d2c357e6b5
parent 59498 50b60f501b05
child 59780 23b67731f4f0
equal deleted inserted replaced
59762:df377a6fdd90 59763:56d2c357e6b5
   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 *)