src/HOL/Lifting_Product.thy
changeset 55085 0e8e4dc55866
parent 55083 0a689157e3ce
child 55414 eab03e9cee8a
     1.1 --- a/src/HOL/Lifting_Product.thy	Mon Jan 20 20:42:43 2014 +0100
     1.2 +++ b/src/HOL/Lifting_Product.thy	Mon Jan 20 21:32:41 2014 +0100
     1.3 @@ -17,15 +17,8 @@
     1.4    "prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
     1.5    by (simp add: prod_pred_def)
     1.6  
     1.7 -lemma prod_rel_eq [relator_eq]:
     1.8 -  shows "prod_rel (op =) (op =) = (op =)"
     1.9 -  by (simp add: fun_eq_iff)
    1.10 -
    1.11 -lemma prod_rel_mono[relator_mono]:
    1.12 -  assumes "A \<le> C"
    1.13 -  assumes "B \<le> D"
    1.14 -  shows "(prod_rel A B) \<le> (prod_rel C D)"
    1.15 -using assms by (auto simp: prod_rel_def)
    1.16 +lemmas prod_rel_eq[relator_eq] = prod.rel_eq
    1.17 +lemmas prod_rel_mono[relator_mono] = prod.rel_mono
    1.18  
    1.19  lemma prod_rel_OO[relator_distr]:
    1.20    "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)"