--- a/src/HOL/IMPP/Hoare.thy Fri Mar 20 11:26:59 2009 +0100
+++ b/src/HOL/IMPP/Hoare.thy Fri Mar 20 15:24:18 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/IMPP/Hoare.thy
- ID: $Id$
Author: David von Oheimb
Copyright 1999 TUM
*)
@@ -219,7 +218,7 @@
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)
prefer 7
apply (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast)
-apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) (thms "hoare_derivs.intros")) THEN_ALL_NEW CLASET' fast_tac) *})
+apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) (thms "hoare_derivs.intros")) THEN_ALL_NEW (fast_tac @{claset})) *})
done
lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}"
@@ -291,7 +290,7 @@
simp_tac @{simpset}, clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
apply (simp_all (no_asm_use) add: triple_valid_def2)
apply (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
-apply (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *}) (* Skip, Ass, Local *)
+apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *}) (* Skip, Ass, Local *)
prefer 3 apply (force) (* Call *)
apply (erule_tac [2] evaln_elim_cases) (* If *)
apply blast+
@@ -336,17 +335,17 @@
lemma MGF_lemma1 [rule_format (no_asm)]: "state_not_singleton ==>
!pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}"
apply (induct_tac c)
-apply (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *})
+apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
prefer 7 apply (fast intro: domI)
apply (erule_tac [6] MGT_alternD)
apply (unfold MGT_def)
apply (drule_tac [7] bspec, erule_tac [7] domI)
-apply (rule_tac [7] escape, tactic {* CLASIMPSET' clarsimp_tac 7 *},
+apply (rule_tac [7] escape, tactic {* clarsimp_tac @{clasimpset} 7 *},
rule_tac [7] P1 = "%Z' s. s= (setlocs Z newlocs) [Loc Arg ::= fun Z]" in hoare_derivs.Call [THEN conseq1], erule_tac [7] conseq12)
apply (erule_tac [!] thin_rl)
apply (rule hoare_derivs.Skip [THEN conseq2])
apply (rule_tac [2] hoare_derivs.Ass [THEN conseq1])
-apply (rule_tac [3] escape, tactic {* CLASIMPSET' clarsimp_tac 3 *},
+apply (rule_tac [3] escape, tactic {* clarsimp_tac @{clasimpset} 3 *},
rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1],
erule_tac [3] conseq12)
apply (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12)
@@ -365,7 +364,7 @@
shows "finite U ==> uG = mgt_call`U ==>
!G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})"
apply (induct_tac n)
-apply (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *})
+apply (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
apply (subgoal_tac "G = mgt_call ` U")
prefer 2
apply (simp add: card_seteq finite_imageI)