src/HOL/NanoJava/Equivalence.thy
changeset 58963 26bf09b95dda
parent 58889 5b7a9633cfa8
child 59498 50b60f501b05
     1.1 --- a/src/HOL/NanoJava/Equivalence.thy	Sun Nov 09 20:49:28 2014 +0100
     1.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Mon Nov 10 21:49:48 2014 +0100
     1.3 @@ -111,7 +111,7 @@
     1.4                   apply fast
     1.5                  apply fast
     1.6                 apply fast
     1.7 -              apply (clarify,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
     1.8 +              apply (clarify,tactic "smp_tac @{context} 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
     1.9               apply fast
    1.10              apply fast
    1.11             apply fast