src/HOL/Fun.thy
changeset 31202 52d332f8f909
parent 31080 21ffc770ebc0
child 31438 a1c4c1500abe
     1.1 --- a/src/HOL/Fun.thy	Mon May 18 15:45:42 2009 +0200
     1.2 +++ b/src/HOL/Fun.thy	Tue May 19 13:57:31 2009 +0200
     1.3 @@ -100,6 +100,9 @@
     1.4  lemma fcomp_id [simp]: "f o> id = f"
     1.5    by (simp add: fcomp_def)
     1.6  
     1.7 +code_const fcomp
     1.8 +  (Eval infixl 1 "#>")
     1.9 +
    1.10  no_notation fcomp (infixl "o>" 60)
    1.11  
    1.12