src/HOL/Algebra/Congruence.thy
changeset 61382 efac889fccbc
parent 44471 3c2b2c4a7c1c
child 63167 0909deb8059b
     1.1 --- a/src/HOL/Algebra/Congruence.thy	Sat Oct 10 16:21:34 2015 +0200
     1.2 +++ b/src/HOL/Algebra/Congruence.thy	Sat Oct 10 16:26:23 2015 +0200
     1.3 @@ -7,15 +7,15 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -section {* Objects *}
     1.8 +section \<open>Objects\<close>
     1.9  
    1.10 -subsection {* Structure with Carrier Set. *}
    1.11 +subsection \<open>Structure with Carrier Set.\<close>
    1.12  
    1.13  record 'a partial_object =
    1.14    carrier :: "'a set"
    1.15  
    1.16  
    1.17 -subsection {* Structure with Carrier and Equivalence Relation @{text eq} *}
    1.18 +subsection \<open>Structure with Carrier and Equivalence Relation @{text eq}\<close>
    1.19  
    1.20  record 'a eq_object = "'a partial_object" +
    1.21    eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".=\<index>" 50)