2011-12-27 haftmann 2011-12-27 be explicit about Finite_Set.fold
2011-09-12 huffman 2011-09-12 simplify proofs using LIMSEQ lemmas
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-08-25 huffman 2011-08-25 rename subset_{interior,closure} to {interior,closure}_mono; remove some legacy theorem names;
2011-08-24 huffman 2011-08-24 move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used
2011-08-23 huffman 2011-08-23 declare euclidean_simps [simp] at the point they are proved; avoid duplicate rule warnings;
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-12 huffman 2011-08-12 remove redundant lemma setsum_norm in favor of norm_setsum; remove finiteness assumption from setsum_norm_le;
2011-08-12 huffman 2011-08-12 make Multivariate_Analysis work with separate set type
2011-08-11 huffman 2011-08-11 avoid duplicate rule warnings
2011-08-10 huffman 2011-08-10 remove several redundant and unused theorems about derivatives
2011-08-09 huffman 2011-08-09 mark some redundant theorems as legacy
2011-05-20 haftmann 2011-05-20 names of fold_set locales resemble name of characteristic property more closely
2011-05-20 haftmann 2011-05-20 use point-free characterization for locale fun_left_comm_idem
2011-03-14 hoelzl 2011-03-14 moved t2_spaces to HOL image
2011-03-13 wenzelm 2011-03-13 eliminated hard tabs;
2011-03-03 hoelzl 2011-03-03 finally remove upper_bound_finite_set
2011-02-28 boehmes 2011-02-28 removed dependency on Dense_Linear_Order
2011-02-25 nipkow 2011-02-25 got rid of lemma upper_bound_finite_set
2011-01-17 boehmes 2011-01-17 made Z3 the default SMT solver again
2011-01-06 boehmes 2011-01-06 differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3"); turned individual SMT solvers into components; made CVC3 the default SMT solver (Z3 is licensed as "non-commercial only"); tuned smt_filter interface
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-11-12 boehmes 2010-11-12 look for certificates relative to the theory
2010-10-26 boehmes 2010-10-26 changed SMT configuration options; updated SMT certificates
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-08-23 hoelzl 2010-08-23 Rewrite the Probability theory. Introduced pinfreal as real numbers with infinity. Use pinfreal as value for measures. Introduces Lebesgue Measure based on the integral in Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure spaces.
2010-07-01 hoelzl 2010-07-01 Add theory for indicator function.
2010-06-21 hoelzl 2010-06-21 Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
2010-05-12 boehmes 2010-05-12 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
2010-05-11 hoelzl 2010-05-11 Removed usage of normalizating locales.
2010-05-09 huffman 2010-05-09 avoid using real-specific versions of generic lemmas
2010-05-07 haftmann 2010-05-07 prefix normalizing replaces class_semiring
2010-04-28 huffman 2010-04-28 remove redundant lemma vector_dist_norm
2010-04-26 huffman 2010-04-26 merged
2010-04-26 huffman 2010-04-26 fix lots of looping simp calls and other warnings
2010-04-25 huffman 2010-04-25 generalize type of continuous_on
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps
2010-04-24 huffman 2010-04-24 document generation for Multivariate_Analysis
2010-04-23 wenzelm 2010-04-23 eliminated spurious schematic statements;
2010-04-21 hoelzl 2010-04-21 Only use provided SMT-certificates in HOL-Multivariate_Analysis.
2010-04-20 himmelma 2010-04-20 Translated remaining theorems about integration from HOL light.
2010-04-07 boehmes 2010-04-07 renamed "smt_record" to "smt_fixed" (somewhat more expressive) and inverted its semantics
2010-03-24 boehmes 2010-03-24 inhibit invokation of external SMT solver
2010-03-09 himmelma 2010-03-09 reset smt_certificates
2010-03-09 himmelma 2010-03-09 added lemmas
2010-03-02 himmelma 2010-03-02 the ordering on real^1 is linear
2010-02-22 hoelzl 2010-02-22 Replaced Integration by Multivariate-Analysis/Real_Integration
2010-02-17 himmelma 2010-02-17 Added integration to Multivariate-Analysis (upto FTC)