moved lemma eq_neq_eq_imp_neq to HOL

--- a/src/HOL/HOL.thy	Wed Nov 08 19:48:34 2006 +0100
+++ b/src/HOL/HOL.thy	Wed Nov 08 19:48:35 2006 +0100
@@ -432,9 +432,10 @@
 by (iprover intro: notI minor major notE)
 
 lemma not_sym: "t ~= s ==> s ~= t"
-apply (erule contrapos_nn)
-apply (erule sym)
-done
+  by (erule contrapos_nn) (erule sym)
+
+lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y"
+  by (erule subst, erule ssubst, assumption)
 
 (*still used in HOLCF*)
 lemma rev_contrapos: