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