src/HOL/Library/Code_Target_Nat.thy
15 months ago haftmann 2018-04-24 proper datatype for 8-bit characters
21 months ago haftmann 2017-10-08 elementary definition of division on natural numbers
2017-06-24 haftmann 2017-06-24 more direct construction of integer_of_num; code equations for integer_of_char may rely on pattern matching on Char
2017-02-07 haftmann 2017-02-07 dedicated computation preprocessing rules for nat, int implemented by target language literals
2016-10-16 haftmann 2016-10-16 more standardized theorem names for facts involving the div and mod identity
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-10-17 haftmann 2015-10-17 qualify some names stemming from internal bootstrap constructions
2015-09-27 haftmann 2015-09-27 monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-02-25 kuncar 2014-02-25 unregister lifting setup following the best practice of Lifting
2013-12-17 haftmann 2013-12-17 avoid clashes of fact names
2013-08-14 Andreas Lochbihler 2013-08-14 use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator
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-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 type lifting setup for code numeral types
2013-02-14 haftmann 2013-02-14 factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions
2013-02-13 haftmann 2013-02-13 explicit conversion integer_of_nat already in Code_Numeral_Types; tuned code postprocessor setup: present arithmetic results as plain numerals without conversions
2012-11-08 haftmann 2012-11-08 refined stack of library theories implementing int and/or nat by target language numerals