more standard notation (like infix);
authorwenzelm
Sun Dec 18 16:13:20 2016 +0100 (2016-12-18)
changeset 6460086e2f2208a58
parent 64599 80ef54198f44
child 64601 37ce6ceacbb7
more standard notation (like infix);
src/HOL/Nonstandard_Analysis/StarDef.thy
     1.1 --- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Dec 18 15:53:27 2016 +0100
     1.2 +++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Dec 18 16:13:20 2016 +0100
     1.3 @@ -81,7 +81,7 @@
     1.4    by (simp add: FreeUltrafilterNat.proper)
     1.5  
     1.6  text \<open>Standard principles that play a central role in the transfer tactic.\<close>
     1.7 -definition Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("_ \<star> _" [300,301] 300)
     1.8 +definition Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("(_ \<star>/ _)" [300, 301] 300)
     1.9    where "Ifun f \<equiv>
    1.10      \<lambda>x. Abs_star (\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})"
    1.11