src/HOL/Tools/numeral.ML
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).