src/HOL/IMPP/Hoare.thy
changeset 27208 5fe899199f85
parent 23894 1a4167d761ac
child 27239 f2f42f9fa09d
     1.1 --- a/src/HOL/IMPP/Hoare.thy	Sat Jun 14 17:49:24 2008 +0200
     1.2 +++ b/src/HOL/IMPP/Hoare.thy	Sat Jun 14 23:19:51 2008 +0200
     1.3 @@ -282,7 +282,9 @@
     1.4  apply          (blast) (* asm *)
     1.5  apply         (blast) (* cut *)
     1.6  apply        (blast) (* weaken *)
     1.7 -apply       (tactic {* ALLGOALS (EVERY'[REPEAT o thin_tac "hoare_derivs ?x ?y", SIMPSET' simp_tac, CLASET' clarify_tac, REPEAT o smp_tac 1]) *})
     1.8 +apply       (tactic {* ALLGOALS (EVERY'
     1.9 +  [REPEAT o RuleInsts.thin_tac @{context} "hoare_derivs ?x ?y",
    1.10 +   simp_tac @{simpset}, clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
    1.11  apply       (simp_all (no_asm_use) add: triple_valid_def2)
    1.12  apply       (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
    1.13  apply      (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *}) (* Skip, Ass, Local *)