src/HOL/Multivariate_Analysis/Integration.thy
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-04-03 hoelzl 2014-04-03 merged DERIV_intros, has_derivative_intros into derivative_intros
2014-04-02 hoelzl 2014-04-02 extend continuous_intros; remove continuous_on_intros and isCont_intros
2014-03-31 hoelzl 2014-03-31 tuned proofs
2014-03-19 haftmann 2014-03-19 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
2014-03-18 hoelzl 2014-03-18 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
2014-03-18 immler 2014-03-18 additional lemmas
2014-03-18 immler 2014-03-18 removed dependencies on theory Ordered_Euclidean_Space
2014-03-18 immler 2014-03-18 use cbox to relax class constraints
2014-03-17 hoelzl 2014-03-17 unify syntax for has_derivative and differentiable
2014-03-17 haftmann 2014-03-17 tuned proofs
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-02-25 wenzelm 2014-02-25 tuned proofs;
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-12-16 immler 2013-12-16 additional lemmas
2013-12-16 immler 2013-12-16 remove redundant constants
2013-12-16 immler 2013-12-16 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
2013-12-16 immler 2013-12-16 prefer box over greaterThanLessThan on euclidean_space
2013-11-12 hoelzl 2013-11-12 stronger inc_induct and dec_induct
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 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-24 wenzelm 2013-09-24 tuned proofs;
2013-09-14 wenzelm 2013-09-14 tuned proofs;
2013-09-14 wenzelm 2013-09-14 tuned proofs;
2013-09-12 huffman 2013-09-12 make 'linear' into a sublocale of 'bounded_linear'; replace 'linear_def' with 'linear_iff'
2013-09-12 huffman 2013-09-12 remove duplicate lemmas
2013-09-11 wenzelm 2013-09-11 tuned proofs;
2013-09-10 wenzelm 2013-09-10 tuned proofs;
2013-09-10 wenzelm 2013-09-10 tuned proofs;
2013-09-10 wenzelm 2013-09-10 tuned proofs;
2013-09-09 wenzelm 2013-09-09 tuned proofs;
2013-09-07 wenzelm 2013-09-07 tuned proofs;
2013-09-06 wenzelm 2013-09-06 tuned proofs;
2013-09-06 wenzelm 2013-09-06 tuned proofs;
2013-09-06 wenzelm 2013-09-06 removed junk;
2013-09-04 wenzelm 2013-09-04 tuned proofs;
2013-09-04 wenzelm 2013-09-04 tuned proofs;
2013-09-04 wenzelm 2013-09-04 tuned proofs;
2013-09-04 wenzelm 2013-09-04 tuned proofs;
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-05-25 haftmann 2013-05-25 weaker precendence of syntax for big intersection and union on sets
2013-04-09 hoelzl 2013-04-09 move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
2013-03-26 hoelzl 2013-03-26 separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
2013-03-23 haftmann 2013-03-23 fundamental revision of big operators on sets
2013-03-22 hoelzl 2013-03-22 introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
2013-03-05 hoelzl 2013-03-05 move lemma Inf to usage point
2013-01-17 wenzelm 2013-01-17 tuned proofs;
2013-01-16 wenzelm 2013-01-16 tuned proofs;
2012-12-14 hoelzl 2012-12-14 Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
2012-12-04 hoelzl 2012-12-04 remove SMT proofs in Multivariate_Analysis
2012-11-28 wenzelm 2012-11-28 eliminated slightly odd identifiers;
2012-11-27 wenzelm 2012-11-27 eliminated some improper identifiers;
2012-11-16 hoelzl 2012-11-16 move theorems to be more generally useable
2012-11-01 blanchet 2012-11-01 regenerated SMT certificates
2012-10-22 wenzelm 2012-10-22 tuned proofs;
2012-10-04 wenzelm 2012-10-04 tuned proofs;