src/HOL/Real.thy
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-08-31 wenzelm 2015-08-31 prefer symbols;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-06-12 haftmann 2015-06-12 uniform _ div _ as infix syntax for ring division
2015-06-01 haftmann 2015-06-01 separate class for division operator, with particular syntax added in more specific classes
2015-04-30 paulson 2015-04-30 tidying some messy proofs
2015-04-09 haftmann 2015-04-09 conversion between division on nat/int and division in archmedean fields
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2015-03-04 nipkow 2015-03-04 Removed the obsolete functions "natfloor" and "natceiling"
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-12 immler 2014-11-12 cancel real of power of numeral also for equality and strict inequality; simplify floor of power of numeral; lemmas about real/floor
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-30 haftmann 2014-10-30 more simp rules concerning dvd and even/odd
2014-10-27 hoelzl 2014-10-27 further generalization of natfloor_div_nat
2014-10-27 hoelzl 2014-10-27 generalize natfloor_div_nat, add floor variant: floor_divide_real_eq_div
2014-09-02 haftmann 2014-09-02 more convenient printing of real numbers after evaluation
2014-08-29 hoelzl 2014-08-29 add simp rules for divisions of numerals in floor and ceiling.
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'
2014-08-28 blanchet 2014-08-28 moved old 'smt' method out of 'Main'
2014-08-25 hoelzl 2014-08-25 introduce real_of typeclass for real :: 'a => real
2014-08-19 hoelzl 2014-08-19 better linarith support for floor, ceiling, natfloor, and natceiling
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-30 hoelzl 2014-06-30 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
2014-06-18 hoelzl 2014-06-18 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
2014-05-07 hoelzl 2014-05-07 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
2014-04-14 hoelzl 2014-04-14 added divide_nonneg_nonneg and co; made it a simp rule
2014-04-12 nipkow 2014-04-12 made mult_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made divide_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-03-19 paulson 2014-03-19 Some rationalisation of basic lemmas
2014-03-13 blanchet 2014-03-13 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-05 hoelzl 2013-11-05 int and nat are conditionally_complete_lattices
2013-11-05 hoelzl 2013-11-05 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
2013-11-05 hoelzl 2013-11-05 generalize bdd_above/below_uminus to ordered_ab_group_add
2013-11-05 hoelzl 2013-11-05 use bdd_above and bdd_below for conditionally complete lattices
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-09-16 kuncar 2013-09-16 use lifting_forget for deregistering numeric types as a quotient type
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-18 wenzelm 2013-08-18 more symbols;
2013-05-13 kuncar 2013-05-13 better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
2013-04-25 hoelzl 2013-04-25 revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
2013-04-24 hoelzl 2013-04-24 spell conditional_ly_-complete lattices correct
2013-03-26 wenzelm 2013-03-26 merged
2013-03-26 hoelzl 2013-03-26 rename RealDef to Real
2013-03-26 hoelzl 2013-03-26 merge RComplete into RealDef
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2010-05-12 boehmes 2010-05-12 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
2010-02-10 haftmann 2010-02-10 moved lemma field_le_epsilon from Real.thy to Fields.thy
2010-02-09 haftmann 2010-02-09 simple proofs make life faster and easier
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-10-05 paulson 2009-10-05 New lemmas connected with the reals and infinite series
2008-12-29 haftmann 2008-12-29 adapted HOL source structure to distribution layout
2008-12-11 nipkow 2008-12-11 codegen
2008-12-10 nipkow 2008-12-10 moved ContNotDenum into Library
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s