| Fri, 24 May 2013 23:57:24 +0200 | haftmann | bookkeeping and input syntax for exact specification of names of symbols in generated code | file | diff | annotate |
| Fri, 24 May 2013 23:57:24 +0200 | haftmann | use generic data for code symbols for unified "code_printing" syntax for custom serialisations | file | diff | annotate |
| Fri, 24 May 2013 23:57:24 +0200 | haftmann | dedicated module for code symbol data | file | diff | annotate |
| Mon, 25 Feb 2013 13:31:02 +0100 | wenzelm | reconsider 'export_code' as "thy_decl" command due to its global side-effect on the file-system; | file | diff | annotate |
| Wed, 22 Aug 2012 22:55:41 +0200 | wenzelm | prefer ML_file over old uses; | file | diff | annotate |
| Thu, 19 Apr 2012 19:36:24 +0200 | haftmann | moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator | file | diff | annotate |
| Thu, 19 Apr 2012 19:18:47 +0200 | haftmann | tuned whitespace | file | diff | annotate |