src/HOL/HOL.thy
changeset 14295 7f115e5c5de4
parent 14248 399a3290936c
child 14357 e49d5d5ae66a
     1.1 --- a/src/HOL/HOL.thy	Sat Dec 13 09:33:52 2003 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Dec 15 16:38:25 2003 +0100
     1.3 @@ -645,6 +645,9 @@
     1.4    "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
     1.5  
     1.6  
     1.7 +lemma Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
     1.8 +by blast
     1.9 +
    1.10  subsubsection {* Monotonicity *}
    1.11  
    1.12  locale mono =
    1.13 @@ -716,6 +719,9 @@
    1.14    apply (erule contrapos_np, simp)
    1.15    done
    1.16  
    1.17 +lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)"  
    1.18 +by (blast intro: order_antisym)
    1.19 +
    1.20  
    1.21  text {* Transitivity. *}
    1.22