src/HOL/Real/Rational.thy
2007-09-20 haftmann 2007-09-20 fixed cg setup
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated IntInf.int, integer);
2007-09-18 haftmann 2007-09-18 renamed constructor RatC to Rational
2007-09-06 berghofe 2007-09-06 Added code generator setup (taken from Library/Executable_Rat.thy, also works for old code generator).
2007-09-01 nipkow 2007-09-01 final(?) iteration of sgn saga.
2007-08-09 haftmann 2007-08-09 adaptions for code generation
2007-07-31 wenzelm 2007-07-31 arith method setup: proper context;
2007-07-20 haftmann 2007-07-20 split class abs from class minus
2007-06-20 huffman 2007-06-20 simplify some proofs
2007-06-13 huffman 2007-06-13 removed constant int :: nat => int; int is now an abbreviation for of_nat :: nat => int
2007-06-12 huffman 2007-06-12 more of_rat lemmas
2007-06-12 huffman 2007-06-12 add function of_rat and related lemmas
2007-03-16 haftmann 2007-03-16 added lattice definitions
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-09-13 huffman 2006-09-13 added instance rat :: recpower
2006-09-06 haftmann 2006-09-06 got rid of Numeral.bin type
2006-06-02 wenzelm 2006-06-02 misc cleanup;
2006-02-09 huffman 2006-02-09 removed redundant lemmas
2006-02-09 huffman 2006-02-09 no longer need All_equiv lemmas
2006-02-02 huffman 2006-02-02 reimplemented using Equiv_Relations.thy
2005-12-08 wenzelm 2005-12-08 tuned proofs;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-07-01 paulson 2004-07-01 new treatment of binary numerals
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-01 wenzelm 2004-05-01 tuned instance statements;
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2004-03-01 paulson 2004-03-01 new Ring_and_Field hierarchy, eliminating redundant axioms
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2004-02-10 paulson 2004-02-10 generic of_nat and of_int functions, and generalization of iszero and neg
2004-01-27 paulson 2004-01-27 replacing HOL/Real/PRat, PNat by the rational number development of Markus Wenzel