2016-08-05 nipkow 2016-08-05 tuned floor lemmas
2016-08-05 nipkow 2016-08-05 more lemmas
2016-08-05 hoelzl 2016-08-05 clean up prove for inter_interior_unions_intervals
2016-08-04 hoelzl 2016-08-04 HOL-Multivariate_Analysis: rename theories for more descriptive names
2016-08-04 hoelzl 2016-08-04 HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
2016-08-03 wenzelm 2016-08-03 include 'begin' and 'end' structure in text folds;
2016-08-02 wenzelm 2016-08-02 tuned proof;
2016-08-02 wenzelm 2016-08-02 proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
2016-08-02 wenzelm 2016-08-02 more symbols;
2016-08-02 wenzelm 2016-08-02 misc tuning and modernization;
2016-08-02 wenzelm 2016-08-02 implicit keyword completion only for actual words (amending 73939a9b70a3);
2016-08-02 wenzelm 2016-08-02 merged
2016-08-02 wenzelm 2016-08-02 tuned;
2016-08-02 wenzelm 2016-08-02 tuned signature -- prover-independence is presently theoretical;
2016-08-02 wenzelm 2016-08-02 tuned;
2016-08-02 wenzelm 2016-08-02 avoid confusion with 'case' and "cases";
2016-08-02 wenzelm 2016-08-02 tuned;
2016-08-02 wenzelm 2016-08-02 clarified: 'imports' is de-facto mandatory;
2016-08-02 wenzelm 2016-08-02 support 'abbrevs' within theory header; simplified 'keywords': no abbreviations here;
2016-08-02 wenzelm 2016-08-02 tuned;
2016-08-02 immler 2016-08-02 more natural definition of type finmap
2016-08-01 wenzelm 2016-08-01 tuned proof;
2016-08-01 wenzelm 2016-08-01 misc tuning and modernization;
2016-08-01 wenzelm 2016-08-01 uniform server startup like windows and macos, for improved robustness if jEdit is terminated abruptly;
2016-08-01 wenzelm 2016-08-01 more restrictive retrieval of rules for matching instead of unification -- relevant for performance of printing terms;
2016-07-31 wenzelm 2016-07-31 misc tuning and modernization;
2016-07-31 wenzelm 2016-07-31 clarified imports;
2016-07-31 wenzelm 2016-07-31 simplified theory structure;
2016-07-31 wenzelm 2016-07-31 misc tuning and modernization;
2016-07-30 wenzelm 2016-07-30 tuned;
2016-07-29 wenzelm 2016-07-29 merged
2016-07-29 wenzelm 2016-07-29 more accurate cong del; tuned proofs;
2016-07-29 traytel 2016-07-29 made generation of transfer goals more robust w.r.t. dead variables
2016-07-29 Andreas Lochbihler 2016-07-29 merged
2016-07-29 Andreas Lochbihler 2016-07-29 prefer [simp] over [iff] as [iff] break HOL-UNITY
2016-07-29 Andreas Lochbihler 2016-07-29 fix LaTeX error
2016-07-29 Andreas Lochbihler 2016-07-29 add lemmas contributed by Peter Gammie
2016-07-29 fleury 2016-07-29 more instantiations for multiset
2016-07-28 wenzelm 2016-07-28 merged
2016-07-28 wenzelm 2016-07-28 misc tuning and modernization;
2016-07-27 wenzelm 2016-07-27 updated to jdk-8u102;
2016-07-28 immler 2016-07-28 numerical bounds on pi
2016-07-24 haftmann 2016-07-24 more on type class hierarchy
2016-07-24 haftmann 2016-07-24 simplified
2016-07-24 haftmann 2016-07-24 text antiquotation for locales (similar to classes)
2016-07-27 Manuel Eberl 2016-07-27 NEWS: Primes
2016-07-26 traytel 2016-07-26 honor sorts in (co)datatype declarations
2016-07-26 wenzelm 2016-07-26 misc tuning and modernization;
2016-07-25 wenzelm 2016-07-25 more symbols;
2016-07-25 wenzelm 2016-07-25 unused (see 1e9e68247ad1);
2016-07-25 wenzelm 2016-07-25 merged
2016-07-22 wenzelm 2016-07-22 misc tuning and modernization;
2016-07-22 wenzelm 2016-07-22 misc tuning and modernization;
2016-07-22 wenzelm 2016-07-22 clarified def vs. ref focus, e.g. for calculation vs. command refs;
2016-07-22 wenzelm 2016-07-22 entity markup for calculation;
2016-07-22 wenzelm 2016-07-22 tuned;
2016-07-22 wenzelm 2016-07-22 more markup for unstructured calculation;
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid improper use of "this";
2016-07-23 nipkow 2016-07-23 added new vcg based on existentially quantified while-rule