# HG changeset patch
# User wenzelm
# Date 1290790455 -3600
# Node ID 3ba17f07b23c241e6330c105ce026affd8a24e23
# Parent  4c17bfdf6f846bfb2cffa774bc2d74403e77d867
lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;

diff -r 4c17bfdf6f84 -r 3ba17f07b23c src/HOL/HOL.thy
--- 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"