src/HOL/Product_Type.thy
changeset 31202 52d332f8f909
parent 30924 c1ed09f3fbfe
child 31604 eb2f9d709296
     1.1 --- a/src/HOL/Product_Type.thy	Mon May 18 15:45:42 2009 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Tue May 19 13:57:31 2009 +0200
     1.3 @@ -726,6 +726,9 @@
     1.4  lemma fcomp_scomp: "(f o> g) o\<rightarrow> h = f o> (g o\<rightarrow> h)"
     1.5    by (simp add: expand_fun_eq scomp_apply fcomp_apply)
     1.6  
     1.7 +code_const scomp
     1.8 +  (Eval infixl 3 "#->")
     1.9 +
    1.10  no_notation fcomp (infixl "o>" 60)
    1.11  no_notation scomp (infixl "o\<rightarrow>" 60)
    1.12