1.1 --- a/src/HOL/Equiv_Relations.thy	Thu Aug 18 13:25:17 2011 +0200
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Aug 18 13:55:26 2011 +0200
     1.3 @@ -164,7 +164,7 @@
     1.4  
     1.5  text{*A congruence-preserving function*}
     1.6  
     1.7 -definition congruent :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"  where
     1.8 +definition congruent :: "('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"  where
     1.9    "congruent r f \<longleftrightarrow> (\<forall>(y, z) \<in> r. f y = f z)"
    1.10  
    1.11  lemma congruentI:
    1.12 @@ -229,7 +229,7 @@
    1.13  
    1.14  text{*A congruence-preserving function of two arguments*}
    1.15  
    1.16 -definition congruent2 :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<times> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" where
    1.17 +definition congruent2 :: "('a \<times> 'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" where
    1.18    "congruent2 r1 r2 f \<longleftrightarrow> (\<forall>(y1, z1) \<in> r1. \<forall>(y2, z2) \<in> r2. f y1 y2 = f z1 z2)"
    1.19  
    1.20  lemma congruent2I':
    1.21 @@ -413,7 +413,7 @@
    1.22  
    1.23  lemma equivpI:
    1.24    "reflp R \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> equivp R"
    1.25 -  by (auto elim: reflpE sympE transpE simp add: equivp_def mem_def)
    1.26 +  by (auto simp add: mem_def elim: reflpE sympE transpE simp add: equivp_def)
    1.27  
    1.28  lemma equivpE:
    1.29    assumes "equivp R"