--- a/src/HOL/ex/Executable_Relation.thy Tue Apr 03 14:09:37 2012 +0200
+++ b/src/HOL/ex/Executable_Relation.thy Tue Apr 03 16:26:48 2012 +0200
@@ -67,11 +67,11 @@
lemma [simp]:
"rel_of_set (set_of_rel S) = S"
-by (rule Quotient_abs_rep[OF Quotient_rel])
+by (rule Quotient3_abs_rep[OF Quotient3_rel])
lemma [simp]:
"set_of_rel (rel_of_set R) = R"
-by (rule Quotient_rep_abs[OF Quotient_rel]) (rule refl)
+by (rule Quotient3_rep_abs[OF Quotient3_rel]) (rule refl)
lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"]