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