--- 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. *}