--- a/src/HOL/Algebra/Congruence.thy Sat Oct 30 21:08:20 2010 +0200
+++ b/src/HOL/Algebra/Congruence.thy Sun Oct 31 11:38:09 2010 +0100
@@ -56,7 +56,8 @@
fixes S (structure)
assumes refl [simp, intro]: "x \<in> carrier S \<Longrightarrow> x .= x"
and sym [sym]: "\<lbrakk> x .= y; x \<in> carrier S; y \<in> carrier S \<rbrakk> \<Longrightarrow> y .= x"
- and trans [trans]: "\<lbrakk> x .= y; y .= z; x \<in> carrier S; y \<in> carrier S; z \<in> carrier S \<rbrakk> \<Longrightarrow> x .= z"
+ and trans [trans]:
+ "\<lbrakk> x .= y; y .= z; x \<in> carrier S; y \<in> carrier S; z \<in> carrier S \<rbrakk> \<Longrightarrow> x .= z"
(* Lemmas by Stephan Hohe *)