src/HOL/Tools/numeral.ML
2014-01-25 haftmann 2014-01-25 prefer explicit code symbol type over ad-hoc name mangling
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
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-28 wenzelm 2013-02-28 just one HOLogic.Trueprop_conv, with regular exception CTERM; tuned;
2012-06-05 haftmann 2012-06-05 prefer records with speaking labels over deeply nested tuples
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-02-15 wenzelm 2012-02-15 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2010-08-31 haftmann 2010-08-31 more coherent naming of syntax data structures
2010-07-19 haftmann 2010-07-19 distinguish different classes of const syntax
2010-01-22 haftmann 2010-01-22 code literals: distinguish numeral classes by different entries
2010-01-14 haftmann 2010-01-14 allow individual printing of numerals during code serialization
2009-12-04 haftmann 2009-12-04 more speaking function names for Code_Printer; added doublesemicolon
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-06-02 haftmann 2009-06-02 tuned whitespace
2009-05-06 haftmann 2009-05-06 robustifed infrastructure for complex term syntax during code generation
2008-10-29 haftmann 2008-10-29 explicit check for pattern discipline before code translation
2008-10-22 haftmann 2008-10-22 code identifier namings are no longer imperative
2008-09-22 haftmann 2008-09-22 fixed headers
2008-09-17 wenzelm 2008-09-17 back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-09-02 haftmann 2008-09-02 distributed literal code generation out of central infrastructure
2008-09-01 haftmann 2008-09-01 restructured code generation of literals
2008-08-28 haftmann 2008-08-28 restructured and split code serializer module
2008-02-17 huffman 2008-02-17 New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
2008-01-25 haftmann 2008-01-25 fixed and tuned
2008-01-21 haftmann 2008-01-21 explicit auxiliary function for code setup
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated IntInf.int, integer);
2007-07-05 wenzelm 2007-07-05 Logical operations on numerals (see also HOL/hologic.ML).