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
--- 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