src/HOL/Hyperreal/StarDef.thy

 constdefs
   star_of :: "'a \<Rightarrow> 'a star"
   "star_of x \<equiv> star_n (\<lambda>n. x)"
 
 text {* Transfer tactic should remove occurrences of @{term star_of} *}
-setup {* [Transfer.add_const "StarDef.star_of"] *}
+setup {* Transfer.add_const "StarDef.star_of" *}
 declare star_of_def [transfer_intro]
 
 lemma star_of_inject: "(star_of x = star_of y) = (x = y)"
 by (transfer, rule refl)
 

 lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))"
 by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star
     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.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))"
 by (simp only: Ifun_star_n)
 

 
 lemma unstar_star_of [simp]: "unstar (star_of p) = p"
 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.add_const "StarDef.unstar" *}
 
 lemma transfer_unstar [transfer_intro]:
   "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
 by (simp only: unstar_star_n)
 

 lemma Iset_star_n:
   "(star_n X \<in> Iset (star_n A)) = ({n. X n \<in> A n} \<in> \<U>)"
 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.add_const "StarDef.Iset" *}
 
 lemma transfer_mem [transfer_intro]:
   "\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
     \<Longrightarrow> x \<in> a \<equiv> {n. X n \<in> A n} \<in> \<U>"
 by (simp only: Iset_star_n)