changeset 49766 | 65318db3087b |
parent 49762 | b5e355c41de3 |
child 49851 | 4d33963962fa |
--- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Wed Oct 10 10:47:52 2012 +0200 +++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Wed Oct 10 10:48:17 2012 +0200 @@ -60,10 +60,8 @@ by simp lemma - "finite {s'. EX s:S. s' = f a e s}" - unfolding Bex_def - apply simp - oops + "finite S ==> finite {s'. EX s:S. s' = f a e s}" + by simp schematic_lemma (* check interaction with schematics *) "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}