src/HOL/Lifting.thy
changeset 47535 0f94b02fda1c
parent 47534 06cc372a80ed
child 47536 8474a865a4e5
--- a/src/HOL/Lifting.thy	Wed Apr 18 10:52:49 2012 +0200
+++ b/src/HOL/Lifting.thy	Wed Apr 18 12:15:20 2012 +0200
@@ -341,6 +341,9 @@
 lemma typedef_right_total: "right_total T"
   unfolding right_total_def T_def by simp
 
+lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
+  unfolding fun_rel_def T_def by simp
+
 lemma typedef_transfer_All: "((T ===> op =) ===> op =) (Ball A) All"
   unfolding T_def fun_rel_def
   by (metis type_definition.Rep [OF type]
@@ -355,7 +358,7 @@
   "((T ===> op =) ===> op =)
     (transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
   unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
-  by (rule typedef_transfer_All [OF assms])
+  by (rule typedef_transfer_All)
 
 end