src/HOL/Nonstandard_Analysis/Star.thy

 theory Star
   imports NSA
 begin
 
 definition  \<comment> \<open>internal sets\<close>
-  starset_n :: "(nat \<Rightarrow> 'a set) \<Rightarrow> 'a star set"  (\<open>*sn* _\<close> [80] 80)
+  starset_n :: "(nat \<Rightarrow> 'a set) \<Rightarrow> 'a star set"
+    (\<open>(\<open>open_block notation=\<open>prefix starset_n\<close>\<close>*sn* _)\<close> [80] 80)
   where "*sn* As = Iset (star_n As)"
 
 definition InternalSets :: "'a star set set"
   where "InternalSets = {X. \<exists>As. X = *sn* As}"
 

   is_starext :: "('a star \<Rightarrow> 'a star) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
   where "is_starext F f \<longleftrightarrow>
     (\<forall>x y. \<exists>X \<in> Rep_star x. \<exists>Y \<in> Rep_star y. y = F x \<longleftrightarrow> eventually (\<lambda>n. Y n = f(X n)) \<U>)"
 
 definition  \<comment> \<open>internal functions\<close>
-  starfun_n :: "(nat \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a star \<Rightarrow> 'b star"  (\<open>*fn* _\<close> [80] 80)
+  starfun_n :: "(nat \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a star \<Rightarrow> 'b star"
+    (\<open>(\<open>open_block notation=\<open>prefix starfun_n\<close>\<close>*fn* _)\<close> [80] 80)
   where "*fn* F = Ifun (star_n F)"
 
 definition InternalFuns :: "('a star => 'b star) set"
   where "InternalFuns = {X. \<exists>F. X = *fn* F}"