--- a/src/HOL/Set.thy Fri Nov 27 16:26:04 2009 +0100
+++ b/src/HOL/Set.thy Fri Nov 27 16:26:23 2009 +0100
@@ -1556,6 +1556,9 @@
lemma imp_refl: "P --> P" ..
+lemma not_mono: "Q --> P ==> ~ P --> ~ Q"
+ by iprover
+
lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)"
by iprover
@@ -1576,9 +1579,6 @@
lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c"
by iprover
-lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c"
- by iprover
-
subsubsection {* Inverse image of a function *}
@@ -1724,7 +1724,6 @@
val contra_subsetD = @{thm contra_subsetD}
val distinct_lemma = @{thm distinct_lemma}
val eq_to_mono = @{thm eq_to_mono}
-val eq_to_mono2 = @{thm eq_to_mono2}
val equalityCE = @{thm equalityCE}
val equalityD1 = @{thm equalityD1}
val equalityD2 = @{thm equalityD2}