# HG changeset patch
# User bulwahn
# Date 1355677649 -3600
# Node ID 768a3fbe4149ddff7f7746032c6b0fb60d5ea230
# Parent  3a4785d64ecbb8347312eebfa497da0a7829b646
providing a custom code equation for vimage to overwrite the vimage definition that would be rewritten by set_comprehension_pointfree simproc in the code preprocessor to an non-terminating code equation

diff -r 3a4785d64ecb -r 768a3fbe4149 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Sun Dec 16 14:19:08 2012 +0100
+++ b/src/HOL/Enum.thy	Sun Dec 16 18:07:29 2012 +0100
@@ -60,6 +60,10 @@
   "Collect P = set (filter P enum)"
   by (simp add: enum_UNIV)
 
+lemma vimage_code [code]:
+  "f -` B = set (filter (%x. f x : B) enum_class.enum)"
+  unfolding vimage_def Collect_code ..
+
 definition card_UNIV :: "'a itself \<Rightarrow> nat"
 where
   [code del]: "card_UNIV TYPE('a) = card (UNIV :: 'a set)"