# HG changeset patch
# User bulwahn
# Date 1349858478 -7200
# Node ID b5e355c41de3736067ded8b029bf14c85e425367
# Parent  b7772f3b6c03eb4a7b637baa5e576a8db4f99d80
adding some example that motivates some of the current changes in the set_comprehension_pointfree simproc

diff -r b7772f3b6c03 -r b5e355c41de3 src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy
--- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Wed Oct 10 10:41:16 2012 +0200
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Wed Oct 10 10:41:18 2012 +0200
@@ -59,6 +59,12 @@
   \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"
   by simp
 
+lemma
+  "finite {s'. EX s:S. s' = f a e s}"
+  unfolding Bex_def
+  apply simp
+  oops
+
 schematic_lemma (* check interaction with schematics *)
   "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
    = finite ((\<lambda>(a:: ?'A, b :: ?'B). Pair_Rep a b) ` (UNIV \<times> UNIV))"