src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Sat Dec 13 09:33:52 2003 +0100
+++ b/src/HOL/HOL.thy	Mon Dec 15 16:38:25 2003 +0100
@@ -645,6 +645,9 @@
   "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
 
 
+lemma Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
+by blast
+
 subsubsection {* Monotonicity *}
 
 locale mono =
@@ -716,6 +719,9 @@
   apply (erule contrapos_np, simp)
   done
 
+lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)"  
+by (blast intro: order_antisym)
+
 
 text {* Transitivity. *}