1.1 --- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Sun Oct 14 19:16:35 2012 +0200
     1.2 +++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Sun Oct 14 19:16:39 2012 +0200
     1.3 @@ -84,6 +84,13 @@
     1.4  apply simp
     1.5  oops
     1.6  
     1.7 +lemma "finite B ==> finite {c. EX x. x : B & c = a * x}"
     1.8 +by simp
     1.9 +
    1.10 +lemma
    1.11 +  "finite A ==> finite B ==> finite {f a * g b |a b. a : A & b : B}"
    1.12 +by simp
    1.13 +
    1.14  schematic_lemma (* check interaction with schematics *)
    1.15    "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
    1.16     = finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))"