src/HOL/Library/Discrete.thy
10 months ago nipkow 2018-09-24 Prefix form of infix with * on either side no longer needs special treatment because (* and *) are no longer comment brackets in terms.
18 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
2017-01-18 paulson 2017-01-18 New material from Bertrand's postulate (file Bertrand_Discrete_Sqrt), and tidied an old messy proof
2016-11-24 eberlm 2016-11-24 Merged natlog2 into Discrete.log
2016-09-01 Manuel Eberl 2016-09-01 Some facts about factorial and binomial coefficients
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
2016-07-16 wenzelm 2016-07-16 tuned proofs;
2016-02-23 nipkow 2016-02-23 more canonical names
2015-12-30 wenzelm 2015-12-30 isabelle update_cartouches -c -t;
2015-12-11 haftmann 2015-12-11 modernized
2015-09-04 wenzelm 2015-09-04 modernized name space management -- more uniform qualification;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-01-11 wenzelm 2015-01-11 tuned -- more Sidekick-friendly layout;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-26 haftmann 2014-10-26 eliminated redundancies; more simp rules
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-02-24 haftmann 2013-02-24 turned example into library for comparing growth of functions
2013-02-17 haftmann 2013-02-17 fundamentals about discrete logarithm and square root