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/MicroJava/BV/Effect.thy
changeset 17088 3f797ec16f02
parent 15481 fc075ae929e4
child 17090 603f23d71ada 
--- a/src/HOL/MicroJava/BV/Effect.thy	Tue Aug 16 19:25:42 2005 +0200
+++ b/src/HOL/MicroJava/BV/Effect.thy	Wed Aug 17 08:06:12 2005 +0200
@@ -407,7 +407,7 @@
 
 lemma xcpt_app_lemma [code]:
   "xcpt_app i G pc et = list_all (is_class G) (xcpt_names (i, G, pc, et))"
-  by (simp add: list_all_conv)
+  by (simp add: list_all_iff)
 
 lemmas [simp del] = app_def xcpt_app_def
isabelle