src/HOL/Archimedean_Field.thy
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