--- 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