src/HOL/NumberTheory/Factorization.thy
2007-07-16 paulson 2007-07-16 tidied using sledgehammer
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-07-01 nipkow 2005-07-01 prime is a predicate now.
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.
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-06-09 paulson 2001-06-09 simplified a proof using new dvd rules
2001-02-04 wenzelm 2001-02-04 HOL-NumberTheory: converted to new-style format and proper document setup;
2000-09-13 paulson 2000-09-13 moved Primes, Fib, Factorization from HOL/ex