src/HOL/NumberTheory/Chinese.thy
2006-08-30 webertj 2006-08-30 lin_arith_prover: splitting reverted because of performance loss
2006-07-31 webertj 2006-07-31 lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-05-17 wenzelm 2006-05-17 prefer 'definition' over low-level defs; tuned source/document;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-10-11 nipkow 2004-10-11 Proofs needed to be updated because induction now preserves name of induction variable.
2004-09-10 nipkow 2004-09-10 Added antisymmetry simproc
2004-01-12 paulson 2004-01-12 Added lemmas to Ring_and_Field with slightly modified simplification rules Deleted some little-used integer theorems, replacing them by the generic ones in Ring_and_Field Consolidated integer powers
2002-08-27 wenzelm 2002-08-27 *** empty log message ***
2002-05-30 nipkow 2002-05-30 Modifications due to enhanced linear arithmetic.
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-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-08-07 paulson 2001-08-07 Tweaks for 1 -> 1'
2001-02-04 wenzelm 2001-02-04 HOL-NumberTheory: converted to new-style format and proper document setup;
2000-08-03 paulson 2000-08-03 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen