src/HOL/Fun.thy
changeset 31202 52d332f8f909
parent 31080 21ffc770ebc0
child 31438 a1c4c1500abe
--- 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)