# HG changeset patch
# User haftmann
# Date 1166426486 -3600
# Node ID c701cdacf69b9523534c4ddad33bf8eb0d05d238
# Parent  c5e79547bf541dba5e6d427c0e07a11d7365547b
infix syntax for generated code for composition

diff -r c5e79547bf54 -r c701cdacf69b src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Dec 18 08:21:25 2006 +0100
+++ b/src/HOL/Fun.thy	Mon Dec 18 08:21:26 2006 +0100
@@ -7,7 +7,7 @@
 header {* Notions about functions *}
 
 theory Fun
-imports Set
+imports Set Code_Generator
 begin
 
 constdefs
@@ -474,6 +474,13 @@
 instance "fun" :: (type, ord) ord ..
 
 
+subsection {* Code generator setup *}
+
+code_const "op \<circ>"
+  (SML infixl 5 "o")
+  (Haskell infixr 9 ".")
+
+
 subsection {* ML legacy bindings *} 
 
 text{*The ML section includes some compatibility bindings and a simproc