src/HOL/Numeral.thy
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated IntInf.int, integer);
2007-09-06 berghofe 2007-09-06 Generalized code generator for numerals.
2007-08-21 huffman 2007-08-21 replace iszero_number_of_Pls with iszero_0 in rel_simps
2007-08-07 haftmann 2007-08-07 new nbe implementation
2007-07-19 haftmann 2007-07-19 tuned
2007-07-10 haftmann 2007-07-10 clarified import
2007-07-05 wenzelm 2007-07-05 added Tools/numeral.ML;
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2007-06-13 huffman 2007-06-13 removed constant int :: nat => int; int is now an abbreviation for of_nat :: nat => int
2007-06-11 huffman 2007-06-11 modify proofs to avoid referring to int::nat=>int
2007-05-31 wenzelm 2007-05-31 moved Integ files to canonical place;
2004-05-21 berghofe 2004-05-21 Adapted to new syntax for case expressions.
2004-03-08 paulson 2004-03-08 generic theorems about exponentials; general tidying up
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2003-12-10 paulson 2003-12-10 Moving some theorems from Real/RealArith0.ML
2002-08-12 nipkow 2002-08-12 Added Mi and Max on sets, hid Min and Pls on numerals.
2002-01-13 wenzelm 2002-01-13 symbolic syntax for x^2 (faills back on plain infix "^");
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-11-08 wenzelm 2001-11-08 use num_const of Pure;
2001-10-22 paulson 2001-10-22 Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.
2001-10-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
2001-10-05 wenzelm 2001-10-05 "num" syntax;
2001-08-08 wenzelm 2001-08-08 constify numeral tokens in order to allow translations;
2000-07-23 wenzelm 2000-07-23 removed selector syntax -- improper tuples are broken beyond repair :-(
2000-07-16 wenzelm 2000-07-16 added syntax for proper / improper selector functions;
2000-06-04 wenzelm 2000-06-04 removed explicit terminator (";");
1999-07-13 paulson 1999-07-13 renamed sort "numeral" to "number"
1999-07-06 wenzelm 1999-07-06 added Numeral.thy, Tools/numeral_syntax.ML;