src/HOL/Code_Evaluation.thy
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-02-05 haftmann 2015-02-05 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-16 blanchet 2014-09-16 added 'extraction' plugins -- this might help 'HOL-Proofs'
2014-09-14 blanchet 2014-09-14 disable datatype 'plugins' for internal types
2014-09-11 blanchet 2014-09-11 updated news
2014-09-03 blanchet 2014-09-03 use 'datatype_new' in 'Main'
2014-08-25 Andreas Lochbihler 2014-08-25 correct code equation for term_of on integer
2014-08-22 Andreas Lochbihler 2014-08-22 add code equation for term_of on integer
2014-05-09 haftmann 2014-05-09 dropped term_of obfuscation -- not really required; tuned theory structure
2014-05-09 haftmann 2014-05-09 hardcoded nbe and sml into value command
2014-05-09 haftmann 2014-05-09 modernized setups
2014-05-09 haftmann 2014-05-09 degeneralized value command into HOL
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-06-02 haftmann 2013-06-02 make reification part of HOL
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-02-15 haftmann 2013-02-15 systematic conversions between nat and nibble/char; more uniform approaches to execute operations on nibble/char
2013-02-15 haftmann 2013-02-15 less customary term_of conversions; spurious side effect on method reflection
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
2013-02-14 haftmann 2013-02-14 reform of predicate compiler / quickcheck theories: implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers! avoid odd New_ prefix by joining related theories; avoid overcompact name DSequence; separated predicate inside random monad into separate theory; consolidated name of theory Quickcheck
2013-02-14 haftmann 2013-02-14 abandoned theory Plain
2012-11-12 haftmann 2012-11-12 tuned import order
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-02-24 haftmann 2012-02-24 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24 haftmann 2012-02-24 given up disfruitful branch
2012-02-23 haftmann 2012-02-23 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2011-05-26 bulwahn 2011-05-26 extending terms of Code_Evaluation by Free to allow partial terms
2010-12-02 haftmann 2010-12-02 corrected representation for code_numeral numerals
2010-12-02 haftmann 2010-12-02 separate term_of function for integers -- more canonical representation of negative integers
2010-11-22 bulwahn 2010-11-22 adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
2010-09-20 haftmann 2010-09-20 dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
2010-09-20 haftmann 2010-09-20 Factored out ML into separate file
2010-09-16 haftmann 2010-09-16 adjusted to changes in Code_Runtime
2010-09-15 haftmann 2010-09-15 Code_Runtime.value, corresponding to ML_Context.value
2010-09-15 haftmann 2010-09-15 code_eval renamed to code_runtime
2010-09-15 haftmann 2010-09-15 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
2010-09-10 bulwahn 2010-09-10 fiddling with the correct setup for String.literal
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-11 haftmann 2010-08-11 moved instantiation target formally to class_target.ML
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-24 haftmann 2010-02-24 evaluation for abstypes
2010-02-22 haftmann 2010-02-22 proper distinction of code datatypes and abstypes
2009-12-07 haftmann 2009-12-07 split off evaluation mechanisms in separte module Code_Eval
2009-11-12 haftmann 2009-11-12 repaired broken code_const for term_of [String.literal]
2009-11-10 wenzelm 2009-11-10 modernized structure Theory_Target;
2009-11-06 bulwahn 2009-11-06 adding tracing function for evaluated code; annotated compilation in the predicate compiler
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-23 haftmann 2009-09-23 Code_Eval(uation)