src/HOL/IMPP/Hoare.thy
changeset 39159 0dec18004e75
parent 35431 8758fe1fc9f8
child 40786 0a54cfc9add3
     1.1 --- a/src/HOL/IMPP/Hoare.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/HOL/IMPP/Hoare.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -218,7 +218,7 @@
     1.4  apply           (rule hoare_derivs.conseq, intro strip, tactic "smp_tac 2 1", clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI)
     1.5  prefer 7
     1.6  apply          (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast)
     1.7 -apply         (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) (thms "hoare_derivs.intros")) THEN_ALL_NEW (fast_tac @{claset})) *})
     1.8 +apply         (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) @{thms hoare_derivs.intros}) THEN_ALL_NEW (fast_tac @{claset})) *})
     1.9  done
    1.10  
    1.11  lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}"
    1.12 @@ -278,7 +278,7 @@
    1.13  
    1.14  lemma hoare_sound: "G||-ts ==> G||=ts"
    1.15  apply (erule hoare_derivs.induct)
    1.16 -apply              (tactic {* TRYALL (eresolve_tac [thm "Loop_sound_lemma", thm "Body_sound_lemma"] THEN_ALL_NEW atac) *})
    1.17 +apply              (tactic {* TRYALL (eresolve_tac [@{thm Loop_sound_lemma}, @{thm Body_sound_lemma}] THEN_ALL_NEW atac) *})
    1.18  apply            (unfold hoare_valids_def)
    1.19  apply            blast
    1.20  apply           blast
    1.21 @@ -349,7 +349,7 @@
    1.22    rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1],
    1.23    erule_tac [3] conseq12)
    1.24  apply         (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12)
    1.25 -apply         (tactic {* (rtac (thm "hoare_derivs.If") THEN_ALL_NEW etac (thm "conseq12")) 6 *})
    1.26 +apply         (tactic {* (rtac @{thm hoare_derivs.If} THEN_ALL_NEW etac @{thm conseq12}) 6 *})
    1.27  apply          (rule_tac [8] hoare_derivs.Loop [THEN conseq2], erule_tac [8] conseq12)
    1.28  apply           auto
    1.29  done