# HG changeset patch
# User haftmann
# Date 1163011715 -3600
# Node ID a268f6288fb65d05fdc7448d4ea3d00fd8fc445f
# Parent  d594c58e24ed9e95b56dda3de7df6c7952886a40
moved lemma eq_neq_eq_imp_neq to HOL

diff -r d594c58e24ed -r a268f6288fb6 src/HOL/HOL.thy
--- 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: