src/HOL/Lifting_Product.thy
changeset 56518 beb3b6851665
parent 56092 1ba075db8fe4
child 56519 c1048f5bbb45
--- a/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:13 2014 +0200
+++ b/src/HOL/Lifting_Product.thy	Thu Apr 10 17:48:14 2014 +0200
@@ -30,13 +30,13 @@
   shows "Domainp (rel_prod T1 T2) = (pred_prod P1 P2)"
 using assms unfolding rel_prod_def pred_prod_def by blast
 
-lemma left_total_rel_prod [reflexivity_rule]:
+lemma left_total_rel_prod [transfer_rule]:
   assumes "left_total R1"
   assumes "left_total R2"
   shows "left_total (rel_prod R1 R2)"
   using assms unfolding left_total_def rel_prod_def by auto
 
-lemma left_unique_rel_prod [reflexivity_rule]:
+lemma left_unique_rel_prod [transfer_rule]:
   assumes "left_unique R1" and "left_unique R2"
   shows "left_unique (rel_prod R1 R2)"
   using assms unfolding left_unique_def rel_prod_def by auto