src/HOL/Archimedean_Field.thy
22 months ago paulson 2017-10-09 new material about connectedness, etc.
24 months ago nipkow 2017-08-26 reorganized and added log-related lemmas
2017-06-21 paulson 2017-06-21 Tidying up integration theory and some new theorems
2016-10-20 eberlm 2016-10-20 More on Fibonacci numbers
2016-09-27 paulson 2016-09-27 a few new theorems and a renaming
2016-09-15 paulson 2016-09-15 simple new lemmas, mostly about sets
2016-08-06 nipkow 2016-08-06 tuned
2016-08-05 nipkow 2016-08-05 fixed floor proofs
2016-08-05 nipkow 2016-08-05 tuned floor lemmas
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
2016-07-14 wenzelm 2016-07-14 misc tuning and modernization;
2016-06-17 hoelzl 2016-06-17 move Conditional_Complete_Lattices to Main
2016-03-15 paulson 2016-03-15 rationalisation of theorem names esp about "real Archimedian" etc.
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2015-12-28 wenzelm 2015-12-28 prefer symbols for "abs";
2015-12-27 wenzelm 2015-12-27 prefer symbols for "floor", "ceiling";
2015-11-23 paulson 2015-11-23 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-02 eberlm 2015-11-02 Rounding function, uniform limits, cotangent, binomial identities
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-08-31 wenzelm 2015-08-31 prefer symbols;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-04-17 haftmann 2015-04-17 compactified proposition
2015-04-09 haftmann 2015-04-09 conversion between division on nat/int and division in archmedean fields
2015-03-05 paulson 2015-03-05 The function frac. Various lemmas about limits, series, the exp function, etc.
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-08-29 hoelzl 2014-08-29 add simp rules for divisions of numerals in floor and ceiling.
2014-08-19 hoelzl 2014-08-19 better linarith support for floor, ceiling, natfloor, and natceiling
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-05 hoelzl 2013-11-05 int and nat are conditionally_complete_lattices
2012-04-18 hoelzl 2012-04-18 add ceiling_diff_floor_le_1
2012-04-03 huffman 2012-04-03 add floor/ceiling lemmas suggested by René Thiemann
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-07-09 bulwahn 2011-07-09 adding code equations to execute floor and ceiling on rational and real numbers
2011-07-09 bulwahn 2011-07-09 adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
2011-07-07 bulwahn 2011-07-07 floor and ceiling definitions are not code equations -- this enables trivial evaluation of floor and ceiling
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-02-26 huffman 2009-02-26 disable floor_minus and ceiling_minus [simp]
2009-02-25 huffman 2009-02-25 new theory of Archimedean fields