--- a/src/HOL/Transfer.thy Sun Apr 22 22:02:52 2012 +0200
+++ b/src/HOL/Transfer.thy Sun Apr 22 21:32:35 2012 +0200
@@ -238,6 +238,16 @@
subsection {* Transfer rules *}
+text {* Transfer rules using implication instead of equality on booleans. *}
+
+lemma eq_imp_transfer [transfer_rule]:
+ "right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
+ unfolding right_unique_alt_def .
+
+lemma forall_imp_transfer [transfer_rule]:
+ "right_total A \<Longrightarrow> ((A ===> op \<longrightarrow>) ===> op \<longrightarrow>) transfer_forall transfer_forall"
+ unfolding right_total_alt_def transfer_forall_def .
+
lemma eq_transfer [transfer_rule]:
assumes "bi_unique A"
shows "(A ===> A ===> op =) (op =) (op =)"
@@ -297,14 +307,4 @@
"bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall"
unfolding transfer_forall_def by (rule All_transfer)
-text {* Transfer rules using implication instead of equality on booleans. *}
-
-lemma eq_imp_transfer [transfer_rule]:
- "right_unique A \<Longrightarrow> (A ===> A ===> op \<longrightarrow>) (op =) (op =)"
- unfolding right_unique_alt_def .
-
-lemma forall_imp_transfer [transfer_rule]:
- "right_total A \<Longrightarrow> ((A ===> op \<longrightarrow>) ===> op \<longrightarrow>) transfer_forall transfer_forall"
- unfolding right_total_alt_def transfer_forall_def .
-
end