src/HOL/Algebra/Divisibility.thy
22 months ago ballarin 2017-08-31 Revert 5a42eddc11c1.
23 months ago haftmann 2017-08-24 swapping of theory dependency yields less pervasive syntax requiring popular symbols \<mu>, \<nu>
23 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2016-12-17 haftmann 2016-12-17 standardized notation
2016-09-19 fleury 2016-09-19 # after multiset intersection and union symbol
2016-09-12 wenzelm 2016-09-12 tuned proofs;
2016-09-11 wenzelm 2016-09-11 tuned proofs;
2016-09-11 wenzelm 2016-09-11 misc tuning and modernization;
2016-09-05 fleury 2016-09-05 add_mset constructor in multisets
2016-08-08 eberlm 2016-08-08 is_prime -> prime
2016-07-20 fleury 2016-07-20 adding mset_map to the simp rules
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2016-02-26 haftmann 2016-02-26 more succint formulation of membership for multisets, similar to lists; discontinued ASCII notation for multiset membership; more theorems on multisets, dropping redundant interpretation; modernized notation; some annotations concerning future work
2015-10-10 wenzelm 2015-10-10 isabelle update_cartouches;
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-06-19 nipkow 2015-06-19 renamed multiset_of -> mset
2015-06-17 nipkow 2015-06-17 renamed Multiset.set_of to the canonical set_mset
2015-06-10 Mathias Fleury 2015-06-10 Renaming multiset operators < ~> <#,...
2015-04-22 nipkow 2015-04-22 added simp rules for ==>
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-09 nipkow 2014-09-09 enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
2014-08-05 wenzelm 2014-08-05 tuned proofs -- fewer warnings;
2014-06-11 Thomas Sewell 2014-06-11 Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.
2014-02-02 paulson 2014-02-02 Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
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.