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