--- a/src/HOL/NSA/StarDef.thy Wed Apr 04 07:47:42 2012 +0200
+++ b/src/HOL/NSA/StarDef.thy Wed Apr 04 09:00:10 2012 +0200
@@ -89,7 +89,7 @@
text {*Initialize transfer tactic.*}
use "transfer.ML"
-setup Transfer.setup
+setup Transfer_Principle.setup
text {* Transfer introduction rules. *}
@@ -167,7 +167,7 @@
"Standard = range star_of"
text {* Transfer tactic should remove occurrences of @{term star_of} *}
-setup {* Transfer.add_const "StarDef.star_of" *}
+setup {* Transfer_Principle.add_const "StarDef.star_of" *}
declare star_of_def [transfer_intro]
@@ -194,7 +194,7 @@
UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
text {* Transfer tactic should remove occurrences of @{term Ifun} *}
-setup {* Transfer.add_const "StarDef.Ifun" *}
+setup {* Transfer_Principle.add_const "StarDef.Ifun" *}
lemma transfer_Ifun [transfer_intro]:
"\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk> \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"
@@ -301,7 +301,7 @@
by (simp add: unstar_def star_of_inject)
text {* Transfer tactic should remove occurrences of @{term unstar} *}
-setup {* Transfer.add_const "StarDef.unstar" *}
+setup {* Transfer_Principle.add_const "StarDef.unstar" *}
lemma transfer_unstar [transfer_intro]:
"p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
@@ -343,7 +343,7 @@
by (simp add: Iset_def starP2_star_n)
text {* Transfer tactic should remove occurrences of @{term Iset} *}
-setup {* Transfer.add_const "StarDef.Iset" *}
+setup {* Transfer_Principle.add_const "StarDef.Iset" *}
lemma transfer_mem [transfer_intro]:
"\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>