# HG changeset patch
# User berghofe
# Date 1259335583 -3600
# Node ID b94b4587106a44def26ad32f6ba361c66482abcf
# Parent  25d6a8982e37c11ffd142dda6941aa6211239bdc
Removed eq_to_mono2, added not_mono.

diff -r 25d6a8982e37 -r b94b4587106a src/HOL/Set.thy
--- 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}