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 theorem
authorpaulson
Wed, 11 Mar 1998 11:05:30 +0100
changeset 4734 6a7c70b053cc
parent 4733 2c984ac036f5
child 4735 6d544b44a70e
new theorem
src/HOL/Vimage.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Vimage.ML	Wed Mar 11 11:05:14 1998 +0100
+++ b/src/HOL/Vimage.ML	Wed Mar 11 11:05:30 1998 +0100
@@ -78,6 +78,11 @@
 qed "UN_vimage";
 Addsimps [UN_vimage];
 
+(*NOT suitable for rewriting*)
+goal thy "f-``B = (UN y: B. f-``{y})";
+by (Blast_tac 1);
+qed "vimage_eq_UN";
+
 
 (** monotonicity **)
isabelle