# HG changeset patch
# User bulwahn
# Date 1333529382 -7200
# Node ID e9274d23ee28104072e79a3b868c3dffc699e38a
# Parent  8fe04753a210174217ccc7236362e493f4f28606# Parent  9f11a3cd84b1c5c701f68a538f384925c033f8ed
merged

diff -r 8fe04753a210 -r e9274d23ee28 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Wed Apr 04 10:17:54 2012 +0200
+++ b/src/HOL/NSA/StarDef.thy	Wed Apr 04 10:49:42 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>
diff -r 8fe04753a210 -r e9274d23ee28 src/HOL/NSA/transfer.ML
--- a/src/HOL/NSA/transfer.ML	Wed Apr 04 10:17:54 2012 +0200
+++ b/src/HOL/NSA/transfer.ML	Wed Apr 04 10:49:42 2012 +0200
@@ -4,14 +4,14 @@
 Transfer principle tactic for nonstandard analysis.
 *)
 
-signature TRANSFER =
+signature TRANSFER_PRINCIPLE =
 sig
   val transfer_tac: Proof.context -> thm list -> int -> tactic
   val add_const: string -> theory -> theory
   val setup: theory -> theory
 end;
 
-structure Transfer: TRANSFER =
+structure Transfer_Principle: TRANSFER_PRINCIPLE =
 struct
 
 structure TransferData = Generic_Data
diff -r 8fe04753a210 -r e9274d23ee28 src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Wed Apr 04 10:17:54 2012 +0200
+++ b/src/HOL/Tools/transfer.ML	Wed Apr 04 10:49:42 2012 +0200
@@ -143,10 +143,10 @@
          (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) i]
   end
 
-val transfer_method =
+val transfer_method : (Proof.context -> Method.method) context_parser =
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_tac ctxt))
 
-val correspondence_method =
+val correspondence_method : (Proof.context -> Method.method) context_parser =
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (correspondence_tac ctxt))
 
 (* Attribute for correspondence rules *)