src/HOL/NanoJava/Equivalence.thy
changeset 59780 23b67731f4f0
parent 59763 56d2c357e6b5
child 59807 22bc39064290
     1.1 --- a/src/HOL/NanoJava/Equivalence.thy	Mon Mar 23 10:16:20 2015 +0100
     1.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Mon Mar 23 13:30:59 2015 +0100
     1.3 @@ -105,8 +105,8 @@
     1.4  apply (rule hoare_ehoare.induct)
     1.5  (*18*)
     1.6  apply (tactic {* ALLGOALS (REPEAT o dresolve_tac @{context} [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *})
     1.7 -apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "hoare ?x ?y") *})
     1.8 -apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "ehoare ?x ?y") *})
     1.9 +apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "hoare ?x ?y" []) *})
    1.10 +apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "ehoare ?x ?y" []) *})
    1.11  apply (simp_all only: cnvalid1_eq cenvalid_def2)
    1.12                   apply fast
    1.13                  apply fast