src/HOL/ex/Codegenerator.thy
2008-10-24 haftmann 2008-10-24 tuned
2008-09-23 haftmann 2008-09-23 renamed rtype to typerep
2007-10-02 haftmann 2007-10-02 ignore mutual recursive modules
2007-09-26 haftmann 2007-09-26 made SML/NJ happy
2007-08-27 haftmann 2007-08-27 circumvented infix problem
2007-08-26 haftmann 2007-08-26 made SML/NJ happy
2007-08-24 haftmann 2007-08-24 overloaded definitions accompanied by explicit constants
2007-08-20 haftmann 2007-08-20 renamed code_gen to export_code
2007-08-13 haftmann 2007-08-13 renamed keyword "to" to "module_name"
2007-08-09 haftmann 2007-08-09 tuned
2007-07-16 haftmann 2007-07-16 added function for case certificates
2007-06-05 wenzelm 2007-06-05 tuned document;
2007-05-06 haftmann 2007-05-06 changed code generator invocation syntax
2007-02-10 haftmann 2007-02-10 splut up code generation in two parts
2006-12-28 haftmann 2006-12-28 removed private files
2006-12-27 haftmann 2006-12-27 added OCaml code generation (without dictionaries)
2006-12-22 haftmann 2006-12-22 deactivated test for the moment
2006-12-21 haftmann 2006-12-21 import path made absolute
2006-12-18 haftmann 2006-12-18 now testing executable content of nearly all HOL
2006-11-27 haftmann 2006-11-27 adjusted syntax for internal code generation
2006-11-24 krauss 2006-11-24 The function package declares the [code] attribute automatically again.
2006-11-22 haftmann 2006-11-22 example tuned
2006-11-18 haftmann 2006-11-18 cleanup
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-13 krauss 2006-11-13 replaced "auto_term" by the simpler method "relation", which does not try to simplify. Some more cleanup.
2006-11-06 haftmann 2006-11-06 code generator module naming improved
2006-11-03 haftmann 2006-11-03 added particular test for partially applied case constants
2006-10-31 haftmann 2006-10-31 adapted to new serializer syntax
2006-10-23 haftmann 2006-10-23 added example with split
2006-10-20 haftmann 2006-10-20 added Haskell
2006-10-16 haftmann 2006-10-16 moved HOL code generator setup to Code_Generator
2006-10-11 haftmann 2006-10-11 added examples for nested let
2006-10-10 haftmann 2006-10-10 stripped pointless head
2006-10-10 haftmann 2006-10-10 changed order
2006-10-01 wenzelm 2006-10-01 tuned;
2006-09-26 haftmann 2006-09-26 renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
2006-09-25 haftmann 2006-09-25 added examples for variable name handling
2006-09-19 haftmann 2006-09-19 code generation 2 adjustments
2006-09-01 haftmann 2006-09-01 final syntax for some Isar code generator keywords
2006-08-14 haftmann 2006-08-14 adaptions to improvements
2006-08-08 haftmann 2006-08-08 added more examples
2006-07-23 haftmann 2006-07-23 small adjustments
2006-06-14 haftmann 2006-06-14 slight adaptions
2006-06-07 haftmann 2006-06-07 slight code generator cleanup
2006-06-06 haftmann 2006-06-06 small fix
2006-05-09 haftmann 2006-05-09 removed 1::int
2006-03-17 haftmann 2006-03-17 added example for operational classes and code generator