src/HOL/Lifting_Sum.thy
changeset 56518 beb3b6851665
parent 55945 e96383acecf9
child 56519 c1048f5bbb45
--- a/src/HOL/Lifting_Sum.thy	Thu Apr 10 17:48:13 2014 +0200
+++ b/src/HOL/Lifting_Sum.thy	Thu Apr 10 17:48:14 2014 +0200
@@ -26,11 +26,11 @@
 using assms
 by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split)
 
-lemma left_total_rel_sum[reflexivity_rule]:
+lemma left_total_rel_sum[transfer_rule]:
   "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (rel_sum R1 R2)"
   using assms unfolding left_total_def split_sum_all split_sum_ex by simp
 
-lemma left_unique_rel_sum [reflexivity_rule]:
+lemma left_unique_rel_sum [transfer_rule]:
   "left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (rel_sum R1 R2)"
   using assms unfolding left_unique_def split_sum_all by simp