src/HOL/Lifting_Product.thy
changeset 55945 e96383acecf9
parent 55944 7ab8f003fe41
child 56092 1ba075db8fe4
--- a/src/HOL/Lifting_Product.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Lifting_Product.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -80,17 +80,17 @@
 interpretation lifting_syntax .
 
 lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair"
-  unfolding fun_rel_def rel_prod_def by simp
+  unfolding rel_fun_def rel_prod_def by simp
 
 lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst"
-  unfolding fun_rel_def rel_prod_def by simp
+  unfolding rel_fun_def rel_prod_def by simp
 
 lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd"
-  unfolding fun_rel_def rel_prod_def by simp
+  unfolding rel_fun_def rel_prod_def by simp
 
 lemma case_prod_transfer [transfer_rule]:
   "((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod"
-  unfolding fun_rel_def rel_prod_def by simp
+  unfolding rel_fun_def rel_prod_def by simp
 
 lemma curry_transfer [transfer_rule]:
   "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
@@ -104,7 +104,7 @@
 lemma rel_prod_transfer [transfer_rule]:
   "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
     rel_prod A C ===> rel_prod B D ===> op =) rel_prod rel_prod"
-  unfolding fun_rel_def by auto
+  unfolding rel_fun_def by auto
 
 end