src/HOL/NanoJava/Equivalence.thy
changeset 37604 1840dc0265da
parent 35417 47ee18b6ae32
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/NanoJava/Equivalence.thy	Mon Jun 28 15:32:25 2010 +0200
     1.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Mon Jun 28 15:32:25 2010 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4   apply  (clarify intro!: Impl_nvalid_0)
     1.5  apply (clarify  intro!: Impl_nvalid_Suc)
     1.6  apply (drule nvalids_SucD)
     1.7 -apply (simp only: all_simps)
     1.8 +apply (simp only: HOL.all_simps)
     1.9  apply (erule (1) impE)
    1.10  apply (drule (2) Impl_sound_lemma)
    1.11   apply  blast