src/HOL/Fun.thy
changeset 61955 e96292f32c3c
parent 61799 4cf66f21b764
child 62390 842917225d56
     1.1 --- a/src/HOL/Fun.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/Fun.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -42,11 +42,11 @@
     1.4  
     1.5  subsection \<open>The Composition Operator \<open>f \<circ> g\<close>\<close>
     1.6  
     1.7 -definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55) where
     1.8 -  "f o g = (\<lambda>x. f (g x))"
     1.9 +definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  (infixl "\<circ>" 55)
    1.10 +  where "f \<circ> g = (\<lambda>x. f (g x))"
    1.11  
    1.12 -notation (xsymbols)
    1.13 -  comp  (infixl "\<circ>" 55)
    1.14 +notation (ASCII)
    1.15 +  comp  (infixl "o" 55)
    1.16  
    1.17  lemma comp_apply [simp]: "(f o g) x = f (g x)"
    1.18    by (simp add: comp_def)