src/HOL/NanoJava/Equivalence.thy
changeset 27208 5fe899199f85
parent 23755 1c4672d130b1
child 27239 f2f42f9fa09d
     1.1 --- a/src/HOL/NanoJava/Equivalence.thy	Sat Jun 14 17:49:24 2008 +0200
     1.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Sat Jun 14 23:19:51 2008 +0200
     1.3 @@ -107,9 +107,9 @@
     1.4  apply (tactic "split_all_tac 1", rename_tac P e Q)
     1.5  apply (rule hoare_ehoare.induct)
     1.6  (*18*)
     1.7 -apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [thm "all_conjunct2", thm "all3_conjunct2"]) *})
     1.8 -apply (tactic {* ALLGOALS (REPEAT o thin_tac "hoare ?x ?y") *})
     1.9 -apply (tactic {* ALLGOALS (REPEAT o thin_tac "ehoare ?x ?y") *})
    1.10 +apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *})
    1.11 +apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "hoare ?x ?y") *})
    1.12 +apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "ehoare ?x ?y") *})
    1.13  apply (simp_all only: cnvalid1_eq cenvalid_def2)
    1.14                   apply fast
    1.15                  apply fast