src/HOL/Algebra/Divisibility.thy
2012-11-08 bulwahn 2012-11-08 tuned proofs
2012-01-06 haftmann 2012-01-06 tuned proofs
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-02 wenzelm 2011-09-02 tuned proofs;
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-05-13 nipkow 2010-05-13 Multiset: renamed, added and tuned lemmas; Permutation: replaced local "remove" by List.remove1
2010-04-22 paulson 2010-04-22 Tidied up using s/l
2010-03-21 wenzelm 2010-03-21 standard headers;
2010-03-21 wenzelm 2010-03-21 slightly more uniform definitions -- eliminated old-style meta-equality;
2010-03-21 wenzelm 2010-03-21 eliminated old constdefs;
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-22 haftmann 2010-02-22 switched notations for pointwise and multiset order
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-08-31 nipkow 2009-08-31 tuned the simp rules for Int involving insert and intervals.
2008-12-16 ballarin 2008-12-16 More porting to new locales.
2008-11-17 haftmann 2008-11-17 tuned unfold_locales invocation
2008-10-15 ballarin 2008-10-15 Removed 'includes' (fixed).
2008-10-15 ballarin 2008-10-15 Removed 'includes'.
2008-08-01 ballarin 2008-08-01 Generalised polynomial lemmas from cring to ring.
2008-07-30 ballarin 2008-07-30 New locales for orders and lattices where the equivalence relation is not restricted to equality.
2008-07-29 ballarin 2008-07-29 New theory on divisibility.