# HG changeset patch
# User bulwahn
# Date 1350234999 -7200
# Node ID 875ed58b3b6597de96eef28297daf13d621255ed
# Parent  caaa1956f0da506ab1368100d190f5631257536e
adding further test cases for the set_comprehension_pointfree simproc

diff -r caaa1956f0da -r 875ed58b3b65 src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy
--- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Sun Oct 14 19:16:35 2012 +0200
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Sun Oct 14 19:16:39 2012 +0200
@@ -84,6 +84,13 @@
 apply simp
 oops
 
+lemma "finite B ==> finite {c. EX x. x : B & c = a * x}"
+by simp
+
+lemma
+  "finite A ==> finite B ==> finite {f a * g b |a b. a : A & b : B}"
+by simp
+
 schematic_lemma (* check interaction with schematics *)
   "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
    = finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))"