--- a/src/HOL/Quotient.thy Fri Mar 23 12:03:59 2012 +0100
+++ b/src/HOL/Quotient.thy Fri Mar 23 14:03:58 2012 +0100
@@ -9,7 +9,7 @@
keywords
"print_quotmaps" "print_quotients" "print_quotconsts" :: diag and
"quotient_type" :: thy_goal and "/" and
- "quotient_definition" :: thy_decl
+ "quotient_definition" :: thy_goal
uses
("Tools/Quotient/quotient_info.ML")
("Tools/Quotient/quotient_type.ML")
@@ -79,6 +79,10 @@
shows "((op =) ===> (op =)) = (op =)"
by (auto simp add: fun_eq_iff elim: fun_relE)
+lemma fun_rel_eq_rel:
+ shows "((op =) ===> R) = (\<lambda>f g. \<forall>x. R (f x) (g x))"
+ by (simp add: fun_rel_def)
+
subsection {* set map (vimage) and set relation *}
definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"