lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;

--- a/src/HOL/HOL.thy	Fri Nov 26 16:28:34 2010 +0100
+++ b/src/HOL/HOL.thy	Fri Nov 26 17:54:15 2010 +0100
@@ -214,6 +214,9 @@
 lemma trans: "[| r=s; s=t |] ==> r=t"
   by (erule subst)
 
+lemma trans_sym [Pure.elim?]: "r = s ==> t = s ==> r = t"
+  by (rule trans [OF _ sym])
+
 lemma meta_eq_to_obj_eq: 
   assumes meq: "A == B"
   shows "A = B"