diff -r ecf9a884970d -r 09d78ec709c7 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Sep 23 12:48:49 2004 +0200
+++ b/src/HOL/Set.thy	Mon Sep 27 10:27:34 2004 +0200
@@ -1086,18 +1086,11 @@
 
 text {* \medskip Monotonicity. *}
 
-lemma mono_Un: includes mono shows "f A \<union> f B \<subseteq> f (A \<union> B)"
-  apply (rule Un_least)
-   apply (rule Un_upper1 [THEN mono])
-  apply (rule Un_upper2 [THEN mono])
-  done
-
-lemma mono_Int: includes mono shows "f (A \<inter> B) \<subseteq> f A \<inter> f B"
-  apply (rule Int_greatest)
-   apply (rule Int_lower1 [THEN mono])
-  apply (rule Int_lower2 [THEN mono])
-  done
-
+lemma mono_Un: "mono f ==> f A \<union> f B \<subseteq> f (A \<union> B)"
+  by (blast dest: monoD)
+
+lemma mono_Int: "mono f ==> f (A \<inter> B) \<subseteq> f A \<inter> f B"
+  by (blast dest: monoD)
 
 subsubsection {* Equalities involving union, intersection, inclusion, etc. *}