--- a/src/HOL/Equiv_Relations.thy Mon Jul 12 08:58:27 2010 +0200
+++ b/src/HOL/Equiv_Relations.thy Mon Jul 12 10:48:37 2010 +0200
@@ -93,7 +93,7 @@
subsection {* Quotients *}
definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set" (infixl "'/'/" 90) where
- [code del]: "A//r = (\<Union>x \<in> A. {r``{x}})" -- {* set of equiv classes *}
+ "A//r = (\<Union>x \<in> A. {r``{x}})" -- {* set of equiv classes *}
lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r"
by (unfold quotient_def) blast