2016-05-26 haftmann 2016-05-26 clarified naming conventions and code for code evaluation sandwiches
2016-04-28 wenzelm 2016-04-28 support 'assumes' in specifications, e.g. 'definition', 'inductive'; tuned signatures;
2016-04-14 wenzelm 2016-04-14 misc tuning and standardization;
2016-04-07 wenzelm 2016-04-07 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; avoid slowdown of Resources.loaded_files due to command name 'use' in Pure base syntax;
2016-04-06 wenzelm 2016-04-06 clarified modules; tuned signature;
2016-04-05 wenzelm 2016-04-05 clarified modules -- simplified bootstrap;
2016-03-07 wenzelm 2016-03-07 File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output; clarified treatment of whitespace in some bash scripts;
2016-03-06 wenzelm 2016-03-06 avoid redundant escapes;
2016-03-01 wenzelm 2016-03-01 tuned signature;
2016-03-01 wenzelm 2016-03-01 clarified modules;
2016-03-01 wenzelm 2016-03-01 load secure.ML earlier; eliminated obsolete ml_parse.ML; tuned signature;
2015-09-01 wenzelm 2015-09-01 thread context for exceptions from forks, e.g. relevant when printing errors; tuned signature;
2015-08-17 wenzelm 2015-08-17 explicit debug flag for ML compiler;
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2015-01-25 wenzelm 2015-01-25 tuned;
2014-12-19 wenzelm 2014-12-19 just one data slot per program unit;
2014-12-19 wenzelm 2014-12-19 proper exception for internal program failure, not user-error;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete Output.urgent_message;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-10-13 wenzelm 2014-10-13 Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
2014-09-08 blanchet 2014-09-08 use compatibility layer
2014-09-05 blanchet 2014-09-05 pretend code generation is a ctr_sugar plugin
2014-09-05 blanchet 2014-09-05 named interpretations
2014-09-01 blanchet 2014-09-01 renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
2014-08-19 blanchet 2014-08-19 reduced dependency on 'Datatype' theory and ML module
2014-05-09 haftmann 2014-05-09 normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>; tuned naming; dropped dead parameters;
2014-03-21 wenzelm 2014-03-21 tuned;
2014-03-13 wenzelm 2014-03-13 added ML antiquotation @{path};
2014-03-06 blanchet 2014-03-06 renamed 'map_pair' to 'map_prod'
2014-02-26 haftmann 2014-02-26 prefer proof context over background theory
2014-02-23 haftmann 2014-02-23 keep only identifiers public which are explicitly requested or demanded by dependencies
2014-02-23 haftmann 2014-02-23 avoid ad-hoc patching of generated code
2014-01-25 haftmann 2014-01-25 prefer explicit code symbol type over ad-hoc name mangling
2013-04-10 wenzelm 2013-04-10 merged
2013-04-10 wenzelm 2013-04-10 more standard module name Axclass (according to file name);
2013-01-22 traytel 2013-01-22 separate data used for case translation from the datatype package
2013-01-22 berghofe 2013-01-22 case translations performed in a separate check phase (with adjustments by traytel)
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2012-11-11 haftmann 2012-11-11 dropped dead code; tuned theory text
2012-08-23 wenzelm 2012-08-23 more basic file dependencies -- no load command here;
2012-07-27 haftmann 2012-07-27 evaluation: allow multiple code modules
2012-07-27 haftmann 2012-07-27 restored narrowing quickcheck after 6efff142bb54
2012-07-16 wenzelm 2012-07-16 more direct Sorts.has_instance; tuned Sorts.mg_domain;
2012-07-16 wenzelm 2012-07-16 comment;
2012-04-30 bulwahn 2012-04-30 adding configuration to pass options to the ghc call in quickcheck[narrowing]
2012-04-04 bulwahn 2012-04-04 rudimentary handling of products in finitize_functions in Quickcheck-Narrowing
2012-03-02 bulwahn 2012-03-02 choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
2012-02-22 bulwahn 2012-02-22 preliminarily switching quickcheck-narrowing off by default (probably it should only be invoked if concrete testing does not work)
2012-01-26 bulwahn 2012-01-26 using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4
2012-01-23 bulwahn 2012-01-23 support for Ex1 in quickcheck-narrowing
2012-01-20 bulwahn 2012-01-20 catching code generation errors in quickcheck-narrowing
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2011-12-29 wenzelm 2011-12-29 comments;
2011-12-20 bulwahn 2011-12-20 generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types; adding common datatype interpretation to quickcheck_common;
2011-12-15 wenzelm 2011-12-15 clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
2011-12-05 bulwahn 2011-12-05 making the default behaviour of quickcheck a little bit less verbose; adapting quickcheck examples
2011-12-05 bulwahn 2011-12-05 inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
2011-12-05 bulwahn 2011-12-05 renaming potential flag to genuine_only flag with an inverse semantics