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.
replaced image_image_eq_UN by image_eq_UN
authorpaulson
Fri, 22 Oct 1999 18:41:00 +0200
changeset 7916 3cb310f40a3a
parent 7915 c7fd7eb3b0ef
child 7917 5e5b9813cce7
replaced image_image_eq_UN by image_eq_UN
src/HOL/Fun.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Fun.ML	Fri Oct 22 18:35:20 1999 +0200
+++ b/src/HOL/Fun.ML	Fri Oct 22 18:41:00 1999 +0200
@@ -67,9 +67,9 @@
 by (Blast_tac 1);
 qed "image_compose";
 
-Goal "f``g``A = (UN x:A. {f (g x)})";
+Goal "f``A = (UN x:A. {f x})";
 by (Blast_tac 1);
-qed "image_image_eq_UN";
+qed "image_eq_UN";
 
 Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
 by (Blast_tac 1);
isabelle