src/HOL/Fun.thy
changeset 37751 89e16802b6cc
parent 36176 3fe7e97ccca8
child 37767 a2b7a20d6ea3
     1.1 --- a/src/HOL/Fun.thy	Thu Jul 08 17:23:05 2010 +0200
     1.2 +++ b/src/HOL/Fun.thy	Fri Jul 09 08:11:10 2010 +0200
     1.3 @@ -95,26 +95,26 @@
     1.4  subsection {* The Forward Composition Operator @{text fcomp} *}
     1.5  
     1.6  definition
     1.7 -  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o>" 60)
     1.8 +  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60)
     1.9  where
    1.10 -  "f o> g = (\<lambda>x. g (f x))"
    1.11 +  "f \<circ>> g = (\<lambda>x. g (f x))"
    1.12  
    1.13 -lemma fcomp_apply:  "(f o> g) x = g (f x)"
    1.14 +lemma fcomp_apply [simp]:  "(f \<circ>> g) x = g (f x)"
    1.15    by (simp add: fcomp_def)
    1.16  
    1.17 -lemma fcomp_assoc: "(f o> g) o> h = f o> (g o> h)"
    1.18 +lemma fcomp_assoc: "(f \<circ>> g) \<circ>> h = f \<circ>> (g \<circ>> h)"
    1.19    by (simp add: fcomp_def)
    1.20  
    1.21 -lemma id_fcomp [simp]: "id o> g = g"
    1.22 +lemma id_fcomp [simp]: "id \<circ>> g = g"
    1.23    by (simp add: fcomp_def)
    1.24  
    1.25 -lemma fcomp_id [simp]: "f o> id = f"
    1.26 +lemma fcomp_id [simp]: "f \<circ>> id = f"
    1.27    by (simp add: fcomp_def)
    1.28  
    1.29  code_const fcomp
    1.30    (Eval infixl 1 "#>")
    1.31  
    1.32 -no_notation fcomp (infixl "o>" 60)
    1.33 +no_notation fcomp (infixl "\<circ>>" 60)
    1.34  
    1.35  
    1.36  subsection {* Injectivity and Surjectivity *}