src/HOL/Quotient.thy
changeset 47544 e455cdaac479
parent 47488 be6dd389639d
child 47579 28f6f4ad69bf
     1.1 --- a/src/HOL/Quotient.thy	Wed Apr 18 15:09:07 2012 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Wed Apr 18 15:48:32 2012 +0200
     1.3 @@ -34,17 +34,6 @@
     1.4    shows "((op =) OOO R) = R"
     1.5    by (auto simp add: fun_eq_iff)
     1.6  
     1.7 -subsection {* Respects predicate *}
     1.8 -
     1.9 -definition
    1.10 -  Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
    1.11 -where
    1.12 -  "Respects R = {x. R x x}"
    1.13 -
    1.14 -lemma in_respects:
    1.15 -  shows "x \<in> Respects R \<longleftrightarrow> R x x"
    1.16 -  unfolding Respects_def by simp
    1.17 -
    1.18  subsection {* set map (vimage) and set relation *}
    1.19  
    1.20  definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"