src/HOL/Lifting_Sum.thy
changeset 55945 e96383acecf9
parent 55943 5c2df04e97d1
child 56518 beb3b6851665
--- a/src/HOL/Lifting_Sum.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Lifting_Sum.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -70,14 +70,14 @@
 interpretation lifting_syntax .
 
 lemma Inl_transfer [transfer_rule]: "(A ===> rel_sum A B) Inl Inl"
-  unfolding fun_rel_def by simp
+  unfolding rel_fun_def by simp
 
 lemma Inr_transfer [transfer_rule]: "(B ===> rel_sum A B) Inr Inr"
-  unfolding fun_rel_def by simp
+  unfolding rel_fun_def by simp
 
 lemma case_sum_transfer [transfer_rule]:
   "((A ===> C) ===> (B ===> C) ===> rel_sum A B ===> C) case_sum case_sum"
-  unfolding fun_rel_def rel_sum_def by (simp split: sum.split)
+  unfolding rel_fun_def rel_sum_def by (simp split: sum.split)
 
 end