src/HOL/Quotient.thy
changeset 47091 d5cd13aca90b
parent 46950 d0181abdbdac
child 47094 1a7ad2601cb5
     1.1 --- a/src/HOL/Quotient.thy	Fri Mar 23 12:03:59 2012 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Fri Mar 23 14:03:58 2012 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  keywords
     1.5    "print_quotmaps" "print_quotients" "print_quotconsts" :: diag and
     1.6    "quotient_type" :: thy_goal and "/" and
     1.7 -  "quotient_definition" :: thy_decl
     1.8 +  "quotient_definition" :: thy_goal
     1.9  uses
    1.10    ("Tools/Quotient/quotient_info.ML")
    1.11    ("Tools/Quotient/quotient_type.ML")
    1.12 @@ -79,6 +79,10 @@
    1.13    shows "((op =) ===> (op =)) = (op =)"
    1.14    by (auto simp add: fun_eq_iff elim: fun_relE)
    1.15  
    1.16 +lemma fun_rel_eq_rel:
    1.17 +  shows "((op =) ===> R) = (\<lambda>f g. \<forall>x. R (f x) (g x))"
    1.18 +  by (simp add: fun_rel_def)
    1.19 +
    1.20  subsection {* set map (vimage) and set relation *}
    1.21  
    1.22  definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"