src/HOL/Set.thy
changeset 13421 8fcdf4a26468
parent 13113 5eb9be7b72a5
child 13462 56610e2ba220
     1.1 --- a/src/HOL/Set.thy	Wed Jul 24 22:14:42 2002 +0200
     1.2 +++ b/src/HOL/Set.thy	Wed Jul 24 22:15:55 2002 +0200
     1.3 @@ -960,16 +960,16 @@
     1.4  
     1.5  text {* \medskip Monotonicity. *}
     1.6  
     1.7 -lemma mono_Un: "mono f ==> f A \<union> f B \<subseteq> f (A \<union> B)"
     1.8 +lemma mono_Un: includes mono shows "f A \<union> f B \<subseteq> f (A \<union> B)"
     1.9    apply (rule Un_least)
    1.10 -   apply (erule Un_upper1 [THEN [2] monoD])
    1.11 -  apply (erule Un_upper2 [THEN [2] monoD])
    1.12 +   apply (rule Un_upper1 [THEN mono])
    1.13 +  apply (rule Un_upper2 [THEN mono])
    1.14    done
    1.15  
    1.16 -lemma mono_Int: "mono f ==> f (A \<inter> B) \<subseteq> f A \<inter> f B"
    1.17 +lemma mono_Int: includes mono shows "f (A \<inter> B) \<subseteq> f A \<inter> f B"
    1.18    apply (rule Int_greatest)
    1.19 -   apply (erule Int_lower1 [THEN [2] monoD])
    1.20 -  apply (erule Int_lower2 [THEN [2] monoD])
    1.21 +   apply (rule Int_lower1 [THEN mono])
    1.22 +  apply (rule Int_lower2 [THEN mono])
    1.23    done
    1.24  
    1.25