src/HOL/RealDef.thy
2011-01-14 wenzelm 2011-01-14 eliminated global prems; tuned proofs;
2010-12-17 bulwahn 2010-12-17 adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
2010-12-06 hoelzl 2010-12-06 move coercions to appropriate places
2010-12-06 nipkow 2010-12-06 moved coercion decl. for int
2010-12-03 wenzelm 2010-12-03 setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
2010-12-01 nipkow 2010-12-01 moved activation of coercion inference into RealDef and declared function real a coercion. Made use of it in theory Ln.
2010-11-30 haftmann 2010-11-30 merged
2010-11-29 haftmann 2010-11-29 replaced slightly odd locale congruent2 by plain definition
2010-11-29 haftmann 2010-11-29 replaced slightly odd locale congruent by plain definition
2010-11-29 haftmann 2010-11-29 equivI has replaced equiv.intro
2010-11-30 huffman 2010-11-30 use new 'file' antiquotation for reference to Dedekind_Real.thy
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-09 blanchet 2010-08-09 replace "setup" with "declaration"
2010-08-06 blanchet 2010-08-06 adapt occurrences of renamed Nitpick functions
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-07-09 haftmann 2010-07-09 nicer xsymbol syntax for fcomp and scomp
2010-06-11 blanchet 2010-06-11 adjust Nitpick's handling of "<" on "rat"s and "reals"
2010-05-17 huffman 2010-05-17 declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
2010-05-15 huffman 2010-05-15 add real_le_linear to list of legacy theorem names
2010-05-11 huffman 2010-05-11 no more RealPow.thy (remaining lemmas moved to RealDef.thy)
2010-05-10 huffman 2010-05-10 add real_mult_commute to legacy theorem names
2010-05-10 huffman 2010-05-10 new construction of real numbers using Cauchy sequences
2010-05-09 huffman 2010-05-09 remove a couple of redundant lemmas; simplify some proofs
2010-04-27 haftmann 2010-04-27 tuned class linordered_field_inverse_zero
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 class division_ring_inverse_zero
2010-03-07 huffman 2010-03-07 add simp rules about Ints, Nats
2010-02-23 huffman 2010-02-23 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-11-13 nipkow 2009-11-13 renamed lemmas "anti_sym" -> "antisym"
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-07-07 nipkow 2009-07-07 renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
2009-06-17 huffman 2009-06-17 merged
2009-06-17 huffman 2009-06-17 new GCD library, courtesy of Jeremy Avigad
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 moved Code_Index, Random and Quickcheck before Main
2009-05-11 haftmann 2009-05-11 tuned interface of Lin_Arith
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-24 huffman 2009-02-24 make more proofs work whether or not One_nat_def is a simp rule
2009-02-21 nipkow 2009-02-21 Removed subsumed lemmas
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s