src/HOL/Real/Rational.thy
2008-09-02 nipkow 2008-09-02 Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and distributed them over Real/ (to do with bijections and density). Library/NatPair became Nat_Int_Bij and made that part of Main.
2008-08-28 haftmann 2008-08-28 no parameter prefix for class interpretation
2008-08-27 huffman 2008-08-27 add lemmas about Rats similar to those about Reals
2008-08-26 nipkow 2008-08-26 Defined rationals (Rats) globally in Rational. Chractarized them with a few lemmas in RealDef, one of them from Sqrt.
2008-07-25 haftmann 2008-07-25 added class preorder
2008-07-21 chaieb 2008-07-21 Tuned and simplified proofs
2008-07-18 haftmann 2008-07-18 refined code generator setup for rational numbers; more simplification rules for rational numbers
2008-07-11 haftmann 2008-07-11 Fract now total; improved code generator setup
2008-07-09 huffman 2008-07-09 rearrange instantiations
2008-04-22 haftmann 2008-04-22 constant HOL.eq now qualified
2008-04-02 haftmann 2008-04-02 explicit class "eq" for operational equality
2008-01-25 haftmann 2008-01-25 improved code theorem setup
2008-01-10 berghofe 2008-01-10 New interface for test data generators.
2008-01-02 haftmann 2008-01-02 splitted class uminus from class minus
2007-12-07 haftmann 2007-12-07 instantiation target rather than legacy instance
2007-11-29 haftmann 2007-11-29 instance command as rudimentary class target
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