src/HOL/Hyperreal/StarDef.thy
changeset 18708 4b3dadb4fe33
parent 17443 f503dccdff27
child 19765 dfe940911617
     1.1 --- a/src/HOL/Hyperreal/StarDef.thy	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Hyperreal/StarDef.thy	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -161,7 +161,7 @@
     1.4    "star_of x \<equiv> star_n (\<lambda>n. x)"
     1.5  
     1.6  text {* Transfer tactic should remove occurrences of @{term star_of} *}
     1.7 -setup {* [Transfer.add_const "StarDef.star_of"] *}
     1.8 +setup {* Transfer.add_const "StarDef.star_of" *}
     1.9  declare star_of_def [transfer_intro]
    1.10  
    1.11  lemma star_of_inject: "(star_of x = star_of y) = (x = y)"
    1.12 @@ -184,7 +184,7 @@
    1.13      UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
    1.14  
    1.15  text {* Transfer tactic should remove occurrences of @{term Ifun} *}
    1.16 -setup {* [Transfer.add_const "StarDef.Ifun"] *}
    1.17 +setup {* Transfer.add_const "StarDef.Ifun" *}
    1.18  
    1.19  lemma transfer_Ifun [transfer_intro]:
    1.20    "\<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))"
    1.21 @@ -234,7 +234,7 @@
    1.22  by (simp add: unstar_def star_of_inject)
    1.23  
    1.24  text {* Transfer tactic should remove occurrences of @{term unstar} *}
    1.25 -setup {* [Transfer.add_const "StarDef.unstar"] *}
    1.26 +setup {* Transfer.add_const "StarDef.unstar" *}
    1.27  
    1.28  lemma transfer_unstar [transfer_intro]:
    1.29    "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
    1.30 @@ -277,7 +277,7 @@
    1.31  by (simp add: Iset_def starP2_star_n)
    1.32  
    1.33  text {* Transfer tactic should remove occurrences of @{term Iset} *}
    1.34 -setup {* [Transfer.add_const "StarDef.Iset"] *}
    1.35 +setup {* Transfer.add_const "StarDef.Iset" *}
    1.36  
    1.37  lemma transfer_mem [transfer_intro]:
    1.38    "\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>