author | haftmann |
Wed, 26 Sep 2007 09:05:58 +0200 | |
changeset 24718 | 16b11ba36350 |
parent 24717 | 56ba87ec8d31 |
child 24719 | 21d1cdab2d8c |
--- a/src/HOL/ex/Codegenerator.thy Tue Sep 25 21:08:36 2007 +0200 +++ b/src/HOL/ex/Codegenerator.thy Wed Sep 26 09:05:58 2007 +0200 @@ -11,6 +11,7 @@ ML {* (*FIXME get rid of this*) nonfix union; nonfix inter; +nonfix upto; *} export_code * in SML module_name CodegenTest @@ -20,6 +21,7 @@ ML {* infix union; infix inter; +infix 4 upto; *} end