Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/NanoJava/Equivalence.thy
changeset 37604 1840dc0265da
parent 35417 47ee18b6ae32
child 51717 9e7d1c139569 
--- a/src/HOL/NanoJava/Equivalence.thy	Mon Jun 28 15:32:25 2010 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy	Mon Jun 28 15:32:25 2010 +0200
@@ -133,7 +133,7 @@
  apply  (clarify intro!: Impl_nvalid_0)
 apply (clarify  intro!: Impl_nvalid_Suc)
 apply (drule nvalids_SucD)
-apply (simp only: all_simps)
+apply (simp only: HOL.all_simps)
 apply (erule (1) impE)
 apply (drule (2) Impl_sound_lemma)
  apply  blast
isabelle