Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
list_all_conv -> iff
authornipkow
Wed, 17 Aug 2005 08:06:12 +0200
changeset 17088 3f797ec16f02
parent 17087 0abf74bdf712
child 17089 f708a31fa8bb
list_all_conv -> iff
src/HOL/MicroJava/BV/Effect.thy file | annotate | diff | comparison | revisions 
--- 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