# HG changeset patch
# User paulson
# Date 919675319 -3600
# Node ID 31483ca40e91dbcad35d4a8379f16e06bb24a3d3
# Parent  062aa156a300220600592430789a35c5651b3f36
new image laws

diff -r 062aa156a300 -r 31483ca40e91 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Mon Feb 22 10:20:25 1999 +0100
+++ b/src/HOL/Fun.ML	Mon Feb 22 10:21:59 1999 +0100
@@ -183,6 +183,14 @@
 by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1);
 qed "surj_imp_inj_inv";
 
+Goal "f``(A Int B) <= f``A Int f``B";
+by (Blast_tac 1);
+qed "image_Int_subset";
+
+Goal "f``A - f``B <= f``(A - B)";
+by (Blast_tac 1);
+qed "image_diff_subset";
+
 Goalw [inj_on_def]
    "[| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
 by (Blast_tac 1);