1.1 --- a/src/HOL/Set.thy	Fri Nov 27 16:26:04 2009 +0100
     1.2 +++ b/src/HOL/Set.thy	Fri Nov 27 16:26:23 2009 +0100
     1.3 @@ -1556,6 +1556,9 @@
     1.4  
     1.5  lemma imp_refl: "P --> P" ..
     1.6  
     1.7 +lemma not_mono: "Q --> P ==> ~ P --> ~ Q"
     1.8 +  by iprover
     1.9 +
    1.10  lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)"
    1.11    by iprover
    1.12  
    1.13 @@ -1576,9 +1579,6 @@
    1.14  lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c"
    1.15    by iprover
    1.16  
    1.17 -lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c"
    1.18 -  by iprover
    1.19 -
    1.20  
    1.21  subsubsection {* Inverse image of a function *}
    1.22  
    1.23 @@ -1724,7 +1724,6 @@
    1.24  val contra_subsetD = @{thm contra_subsetD}
    1.25  val distinct_lemma = @{thm distinct_lemma}
    1.26  val eq_to_mono = @{thm eq_to_mono}
    1.27 -val eq_to_mono2 = @{thm eq_to_mono2}
    1.28  val equalityCE = @{thm equalityCE}
    1.29  val equalityD1 = @{thm equalityD1}
    1.30  val equalityD2 = @{thm equalityD2}