# HG changeset patch
# User oheimb
# Date 997345065 -7200
# Node ID f3ff2549cdc8af0956fedb29e245f3f2fe5a57a6
# Parent  6659e1ddd4ca7929dfbf81b3ca7d5a195ec48657
added pair_imageI (also as intro rule)

diff -r 6659e1ddd4ca -r f3ff2549cdc8 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Aug 09 10:16:23 2001 +0200
+++ b/src/HOL/Product_Type.thy	Thu Aug 09 10:17:45 2001 +0200
@@ -30,9 +30,9 @@
 qed
 
 syntax (symbols)
-  "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
+  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
 syntax (HTML output)
-  "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
+  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
 
 
 (* abstract constants and syntax *)
@@ -74,8 +74,8 @@
   "A <*> B"      => "Sigma A (_K B)"
 
 syntax (symbols)
-  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\\<Sigma> _\\<in>_./ _)"   10)
-  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \\<times> _" [81, 80] 80)
+  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
+  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
 
 print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
 
@@ -118,6 +118,11 @@
 
 use "Product_Type_lemmas.ML"
 
+lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
+apply (rule_tac x = "(a,b)" in image_eqI)
+apply  auto
+done
+
 constdefs
   internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c"
   "internal_split == split"