Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New, stronger rewrites
authorpaulson
Thu, 12 Mar 1998 10:40:08 +0100
changeset 4738 699a91d01d6d
parent 4737 4544290d5a6b
child 4739 50457d3b80e2
New, stronger rewrites
src/HOL/Vimage.ML file | annotate | diff | comparison | revisions 
--- 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);
isabelle