src/HOL/Equiv_Relations.thy
 changeset 44278 1220ecb81e8f parent 44204 3cdc4176638c child 44279 7496258e44e4
```     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"
```