| changeset 4738 | 699a91d01d6d |
| parent 4734 | 6a7c70b053cc |
| child 5069 | 3ea049f7979d |
--- 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);