src/HOL/Set.thy
 changeset 33935 b94b4587106a parent 33533 40b44cb20c8c child 34209 c7f621786035
```     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}
```