src/HOL/Rational.thy
2010-02-09 haftmann 2010-02-09 dropped lemma duplicates
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-11-20 nipkow 2009-11-20 Rene tuned proof
2009-11-20 nipkow 2009-11-20 added Rene Thiemann's normalize function
2009-10-26 wenzelm 2009-10-26 tuned white space;
2009-10-23 blanchet 2009-10-23 continuation of Nitpick's integration into Isabelle; added examples, and integrated non-Main theories better.
2009-09-23 haftmann 2009-09-23 Code_Eval(uation)
2009-07-14 haftmann 2009-07-14 prefer code_inline over code_unfold; use code_unfold_post where appropriate
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-06-17 huffman 2009-06-17 merged
2009-06-17 huffman 2009-06-17 new GCD library, courtesy of Jeremy Avigad
2009-06-17 haftmann 2009-06-17 obey SML syntax even more closely
2009-06-17 haftmann 2009-06-17 obey SML syntax more closely
2009-06-16 haftmann 2009-06-16 denominator should not be zero
2009-06-15 haftmann 2009-06-15 hide constant Quickcheck.random
2009-05-19 haftmann 2009-05-19 String.literal replaces message_string, code_numeral replaces (code_)index
2009-05-19 haftmann 2009-05-19 moved Code_Index, Random and Quickcheck before Main
2009-05-11 haftmann 2009-05-11 tuned interface of Lin_Arith
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-04-28 haftmann 2009-04-28 stripped class recpower further
2009-04-22 haftmann 2009-04-22 power operation defined generic
2009-03-22 nipkow 2009-03-22 1. New cancellation simprocs for common factors in inequations 2. Updated the documentation
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-02 nipkow 2009-03-02 name changes
2009-02-25 huffman 2009-02-25 generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
2009-02-25 huffman 2009-02-25 add lemmas about comparisons of Fract a b with 0 and 1
2009-02-16 haftmann 2009-02-16 more default simp rules for sgn
2009-02-15 nipkow 2009-02-15 dvd and setprod lemmas
2009-02-12 huffman 2009-02-12 move countability proof from Rational to Countable; add instance rat :: countable
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2009-01-02 haftmann 2009-01-02 named code theorem for Fract_norm
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s