--- a/src/HOL/Fun.thy Mon May 18 15:45:42 2009 +0200
+++ b/src/HOL/Fun.thy Tue May 19 13:57:31 2009 +0200
@@ -100,6 +100,9 @@
lemma fcomp_id [simp]: "f o> id = f"
by (simp add: fcomp_def)
+code_const fcomp
+ (Eval infixl 1 "#>")
+
no_notation fcomp (infixl "o>" 60)
--- 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)