src/HOL/NumberTheory/EulerFermat.thy
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-05-17 wenzelm 2006-05-17 prefer 'definition' over low-level defs; tuned source/document;
2005-12-08 wenzelm 2005-12-08 tuned sources and proofs
2005-07-07 nipkow 2005-07-07 linear arithmetic now takes "&" in assumptions apart.
2005-07-01 nipkow 2005-07-01 prime is a predicate now.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-12-12 nipkow 2004-12-12 REorganized Finite_Set
2004-12-09 nipkow 2004-12-09 First step in reorganizing Finite_Set
2004-09-10 nipkow 2004-09-10 Added antisymmetry simproc
2004-06-24 paulson 2004-06-24 replaced monomorphic abs definitions by abs_if
2003-08-29 ballarin 2003-08-29 Methods rule_tac etc support static (Isar) contexts.
2003-02-26 paulson 2003-02-26 zprime_def fixes by Jeremy Avigad
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-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
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;
2001-01-09 nipkow 2001-01-09 *** empty log message ***
2000-08-03 paulson 2000-08-03 Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen