# HG changeset patch
# User paulson
# Date 886420539 -3600
# Node ID 6fc8f224655fe756381167cf3c3eb5399357fb1c
# Parent  ff0c5c57fdfbd33253919a210923aa6c81e62006
Three new facts about Image

diff -r ff0c5c57fdfb -r 6fc8f224655f src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Mon Feb 02 12:48:11 1998 +0100
+++ b/src/HOL/Relation.ML	Mon Feb 02 12:55:39 1998 +0100
@@ -171,6 +171,22 @@
 AddIs  [ImageI];
 AddSEs [ImageE];
 
+
+qed_goal "Image_empty" Relation.thy
+    "R^^{} = {}"
+ (fn _ => [ Blast_tac 1 ]);
+
+Addsimps [Image_empty];
+
+qed_goal "Image_Int_subset" Relation.thy
+    "R ^^ (A Int B) <= R ^^ A Int R ^^ B"
+ (fn _ => [ Blast_tac 1 ]);
+
+qed_goal "Image_Un" Relation.thy
+    "R ^^ (A Un B) = R ^^ A Un R ^^ B"
+ (fn _ => [ Blast_tac 1 ]);
+
+
 qed_goal "Image_subset" Relation.thy
     "!!A B r. r <= A Times B ==> r^^C <= B"
  (fn _ =>