src/HOL/Real.thy
20 months ago immler 2017-10-24 generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
20 months ago paulson 2017-10-09 new material about connectedness, etc.
21 months ago nipkow 2017-08-26 reorganized and added log-related lemmas
24 months ago haftmann 2017-06-20 stripped code pre/postprocessor setup for real from superfluous rules
2017-05-21 blanchet 2017-05-21 added one more simplification to help replay
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-29 boehmes 2016-09-29 invoke argo as part of the tried automatic proof methods
2016-09-29 boehmes 2016-09-29 new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
2016-08-12 wenzelm 2016-08-12 more symbols;
2016-08-05 nipkow 2016-08-05 added missing lemmas
2016-08-05 nipkow 2016-08-05 tuned floor lemmas
2016-07-15 wenzelm 2016-07-15 misc tuning and modernization;
2016-06-23 wenzelm 2016-06-23 misc tuning and modernization;
2016-06-17 hoelzl 2016-06-17 move Conditional_Complete_Lattices to Main
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-03-16 paulson 2016-03-16 Contractible sets. Also removal of obsolete theorems and refactoring
2016-03-15 paulson 2016-03-15 rationalisation of theorem names esp about "real Archimedian" etc.
2016-02-24 paulson 2016-02-24 Merge
2016-02-24 paulson 2016-02-24 Substantial new material for multivariate analysis. Also removal of some duplicates.
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2016-02-17 haftmann 2016-02-17 generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
2016-01-06 hoelzl 2016-01-06 add the proof of the central limit theorem
2016-01-06 blanchet 2016-01-06 more complete setup for 'Rat' in Nitpick
2015-12-28 wenzelm 2015-12-28 prefer symbols for "abs";
2015-12-27 wenzelm 2015-12-27 prefer symbols for "floor", "ceiling";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-17 paulson 2015-11-17 Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-09-30 paulson 2015-09-30 real_of_nat_Suc is now a simprule
2015-09-21 paulson 2015-09-21 new lemmas and movement of lemmas into place
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