author | haftmann |
Sun, 26 Aug 2007 14:37:18 +0200 | |
changeset 24430 | df56b9779a3d |
parent 24429 | 76372c3847a2 |
child 24431 | 02d29baa42ff |
--- a/src/HOL/ex/Codegenerator.thy Sun Aug 26 01:19:20 2007 +0200 +++ b/src/HOL/ex/Codegenerator.thy Sun Aug 26 14:37:18 2007 +0200 @@ -8,6 +8,11 @@ imports ExecutableContent begin +ML {* +nonfix union; +nonfix inter; +*} + export_code * in SML module_name CodegenTest in OCaml file - in Haskell file -