# HG changeset patch
# User ballarin
# Date 1288521489 -3600
# Node ID cd932ab8cb596dcf6ddb11e03e8fc5feb86545c1
# Parent  ba13793594f079cc5dd23316d2420570a73fe396
Minor reformat.

diff -r ba13793594f0 -r cd932ab8cb59 src/HOL/Algebra/Congruence.thy
--- 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 *)
 
diff -r ba13793594f0 -r cd932ab8cb59 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Sat Oct 30 21:08:20 2010 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Sun Oct 31 11:38:09 2010 +0100
@@ -24,7 +24,8 @@
     and le_trans [trans]:
       "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
     and le_cong:
-      "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
+      "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow>
+      x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
 
 definition
   lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)