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