diff -r 96699d8eb49e -r 21bbd410ba04 src/HOL/Algebra/Congruence.thy
--- a/src/HOL/Algebra/Congruence.thy	Fri Aug 01 17:41:37 2008 +0200
+++ b/src/HOL/Algebra/Congruence.thy	Fri Aug 01 18:10:52 2008 +0200
@@ -9,12 +9,13 @@
 
 section {* Objects *}
 
-text {* Structure with a carrier set. *}
+subsection {* Structure with Carrier Set. *}
 
 record 'a partial_object =
   carrier :: "'a set"
 
-text {* Dito with equivalence relation *}
+
+subsection {* Structure with Carrier and Equivalence Relation @{text eq} *}
 
 record 'a eq_object = "'a partial_object" +
   eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".=\<index>" 50)
@@ -45,15 +46,14 @@
   "x .\<notin>\<index> A" == "~(x .\<in>\<index> A)"
   "A {.\<noteq>}\<index> B" == "~(A {.=}\<index> B)"
 
-
-section {* Equivalence Relations *}
-
 locale equivalence =
   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"
 
+(* Lemmas by Stephan Hohe *)
+
 lemma elemI:
   fixes R (structure)
   assumes "a' \<in> A" and "a .= a'"
@@ -205,6 +205,7 @@
 by fast
 
 (* FIXME: the following two required in Isabelle 2008, not Isabelle 2007 *)
+(* alternatively, could declare lemmas [trans] = ssubst [where 'a = "'a set"] *)
 
 lemma (in equivalence) equal_set_eq_trans [trans]:
   assumes AB: "A = B" and BC: "B {.=} C"
@@ -216,6 +217,7 @@
   shows "A {.=} C"
   using AB BC by simp
 
+
 lemma (in equivalence) set_eq_trans [trans]:
   assumes AB: "A {.=} B" and BC: "B {.=} C"
     and carr: "A \<subseteq> carrier S"  "B \<subseteq> carrier S"  "C \<subseteq> carrier S"