src/Tools/Code_Generator.thy
2014-06-28 haftmann 2014-06-28 tracing facilities for the code generator preprocessor
2014-05-15 haftmann 2014-05-15 modernized setup
2014-05-09 haftmann 2014-05-09 degeneralized value command into HOL
2014-02-09 haftmann 2014-02-09 dropped legacy finally
2014-01-01 haftmann 2014-01-01 fundamental treatment of undefined vs. universally partial replaces code_abort
2013-05-24 haftmann 2013-05-24 bookkeeping and input syntax for exact specification of names of symbols in generated code
2013-05-24 haftmann 2013-05-24 use generic data for code symbols for unified "code_printing" syntax for custom serialisations
2013-05-24 haftmann 2013-05-24 dedicated module for code symbol data
2013-02-25 wenzelm 2013-02-25 reconsider 'export_code' as "thy_decl" command due to its global side-effect on the file-system;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-19 haftmann 2012-04-19 moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator
2012-04-19 haftmann 2012-04-19 tuned whitespace
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-03-15 wenzelm 2012-03-15 declare minor keywords via theory header;
2011-10-19 bulwahn 2011-10-19 removing old code generator
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-08-10 wenzelm 2011-08-10 moved old code generator to src/Tools/;
2011-07-01 bulwahn 2011-07-01 adding a value antiquotation
2011-06-27 wenzelm 2011-06-27 document antiquotations are managed as theory data, with proper name space and entity markup;
2011-05-27 blanchet 2011-05-27 renamed "Auto_Tools" "Try"
2010-10-25 blanchet 2010-10-25 introduced manual version of "Auto Solve" as "solve_direct"
2010-10-01 haftmann 2010-10-01 moved ML_Context.value to Code_Runtime
2010-09-16 haftmann 2010-09-16 adjusted setup
2010-09-15 haftmann 2010-09-15 load code_runtime immediately again
2010-09-15 haftmann 2010-09-15 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
2010-09-15 haftmann 2010-09-15 code_eval renamed to code_runtime
2010-09-11 blanchet 2010-09-11 make Auto Solve part of the "Auto Tools"
2010-09-11 blanchet 2010-09-11 start renaming "Auto_Counterexample" to "Auto_Tools"; Auto Sledgehammer now uses so the name is clearly wrong
2010-09-01 haftmann 2010-09-01 factored out generic part of Scala serializer into code_namespace.ML
2010-07-14 haftmann 2010-07-14 load cache_io before code generator; moved adhoc-overloading to generic tools
2010-06-15 haftmann 2010-06-15 added code_simp infrastructure
2010-01-27 haftmann 2010-01-27 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
2010-01-08 haftmann 2010-01-08 a primitive scala serializer
2009-12-07 haftmann 2009-12-07 split off evaluation mechanisms in separte module Code_Eval
2009-11-24 wenzelm 2009-11-24 some rearangement of load order to keep preferences adjacent -- slightly fragile;
2009-11-20 wenzelm 2009-11-20 load ML directly into theory Code_Generator (quickcheck also requires this);
2009-10-28 blanchet 2009-10-28 introduced Auto Nitpick in addition to Auto Quickcheck; this required generalizing the theorem hook used by Quickcheck, following a suggestion by Florian
2009-06-23 haftmann 2009-06-23 uniformly capitialized names for subdirectories
2009-05-12 haftmann 2009-05-12 transferred code generator preprocessor into separate module
2009-05-04 haftmann 2009-05-04 removed code_name module
2009-04-24 haftmann 2009-04-24 observe distinction between Pure/Tools and Tools more closely
2009-04-15 haftmann 2009-04-15 code generator bootstrap theory src/Tools/Code_Generator.thy