# HG changeset patch
# User huffman
# Date 1335123155 -7200
# Node ID ead185e60b8c18b152b7cc821de80cf04a520947
# Parent  9904aad07afa852cbdbebea38d08d904504f4317
tuned precedence order of transfer rules

diff -r 9904aad07afa -r ead185e60b8c src/HOL/Transfer.thy
--- 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