src/HOL/Code_Evaluation.thy
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)