src/HOL/NumberTheory/IntFact.thy
2005-12-08 wenzelm 2005-12-08 tuned sources and proofs
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-12-09 nipkow 2004-12-09 First step in reorganizing Finite_Set
2003-12-03 paulson 2003-12-03 Simplification of the development of Integers
2002-07-24 wenzelm 2002-07-24 simplified locale predicates;
2002-07-19 wenzelm 2002-07-19 *** empty log message ***
2002-07-16 wenzelm 2002-07-16 adapted to locale defs;
2002-01-10 wenzelm 2002-01-10 qualified exports from locales;
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-09-04 wenzelm 2001-09-04 renamed "antecedent" case to "rule_context";
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