changeset 24430 | df56b9779a3d |
parent 24423 | ae9cd0e92423 |
child 24432 | d555d941f983 |
--- 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 -