# HG changeset patch
# User paulson
# Date 889695608 -3600
# Node ID 699a91d01d6da3a48f56e2eb65a232a92c0d55a8
# Parent  4544290d5a6b89ab0ff3088f4a9306a60bd40865
New, stronger rewrites

diff -r 4544290d5a6b -r 699a91d01d6d src/HOL/Vimage.ML
--- a/src/HOL/Vimage.ML	Thu Mar 12 10:39:19 1998 +0100
+++ b/src/HOL/Vimage.ML	Thu Mar 12 10:40:08 1998 +0100
@@ -64,9 +64,13 @@
 by (Blast_tac 1);
 qed "vimage_insert";
 
-goal thy "f-``(A Int B) <= (f-``A) Int (f-``B)";
+goal thy "f-``(A Int B) = (f-``A) Int (f-``B)";
 by (Blast_tac 1);
-qed "vimage_Int_subset";
+qed "vimage_Int";
+
+goal thy "f-``(A-B) = (f-``A) - (f-``B)";
+by (Blast_tac 1);
+qed "vimage_Diff";
 
 goal thy "f-``UNIV = UNIV";
 by (Blast_tac 1);