--- a/src/HOL/Lifting_Option.thy Thu Apr 10 17:48:13 2014 +0200
+++ b/src/HOL/Lifting_Option.thy Thu Apr 10 17:48:14 2014 +0200
@@ -39,11 +39,11 @@
using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
by (auto iff: fun_eq_iff split: option.split)
-lemma left_total_rel_option[reflexivity_rule]:
+lemma left_total_rel_option[transfer_rule]:
"left_total R \<Longrightarrow> left_total (rel_option R)"
unfolding left_total_def split_option_all split_option_ex by simp
-lemma left_unique_rel_option [reflexivity_rule]:
+lemma left_unique_rel_option [transfer_rule]:
"left_unique R \<Longrightarrow> left_unique (rel_option R)"
unfolding left_unique_def split_option_all by simp