2014-05-21 blanchet 2014-05-21 added comment
2014-05-21 blanchet 2014-05-21 move exhaust first, for technical reasons
2014-05-21 blanchet 2014-05-21 avoid markup-generating @{make_string}
2014-05-21 hoelzl 2014-05-21 generalized Bochner integral over infinite sums
2014-05-21 wenzelm 2014-05-21 unused;
2014-05-21 wenzelm 2014-05-21 obsolete;
2014-05-21 wenzelm 2014-05-21 approximative update of versions;
2014-05-21 wenzelm 2014-05-21 incorporate isabelle.graphview into Pure.jar, which saves 20..30s build time; discontinued pointless "isabelle graphview" command-line tool (Proof General legacy);
2014-05-21 Lars Hupel 2014-05-21 remove stray println;
2014-05-20 blanchet 2014-05-20 CONTRIBUTORS
2014-05-20 blanchet 2014-05-20 added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
2014-05-20 blanchet 2014-05-20 added Isabelle system option 'mash'
2014-05-20 wenzelm 2014-05-20 updated cygwin;
2014-05-20 wenzelm 2014-05-20 afford strict check (see also AFP/a8e08d947f0a);
2014-05-20 hoelzl 2014-05-20 add various lemmas
2014-05-20 wenzelm 2014-05-20 merged
2014-05-20 wenzelm 2014-05-20 merged
2014-05-20 wenzelm 2014-05-20 adhoc move to lxbroy10, which has 120 GB more memory than lxbroy2;
2014-05-20 wenzelm 2014-05-20 explicit treatment of unfinished cartouches, which is important for Thy_Syntax.consolidate_spans;
2014-05-20 blanchet 2014-05-20 news
2014-05-20 blanchet 2014-05-20 updated docs
2014-05-20 blanchet 2014-05-20 more flexible environment variable
2014-05-20 blanchet 2014-05-20 tuning
2014-05-20 nipkow 2014-05-20 added unit :: linorder
2014-05-20 nipkow 2014-05-20 added lemma
2014-05-20 blanchet 2014-05-20 implemented MaSh/SML hints
2014-05-20 blanchet 2014-05-20 better way to take invisible facts into account than 'island' business
2014-05-20 blanchet 2014-05-20 cleaner handling of learned proofs
2014-05-20 blanchet 2014-05-20 implemented learning of single proofs in SML MaSh
2014-05-19 blanchet 2014-05-19 take weights into consideration in knn
2014-05-19 blanchet 2014-05-19 added SML implementation of MaSh
2014-05-19 blanchet 2014-05-19 use E 1.8's auto scheduler option
2014-05-19 blanchet 2014-05-19 started work on MaSh/SML
2014-05-19 blanchet 2014-05-19 tune
2014-05-19 blanchet 2014-05-19 store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
2014-05-19 Lars Hupel 2014-05-19 trace windows uses search feature of Pretty_Text_Area; recursive invocations and intermediate steps are now shown in order; refinements to the exclusion of uninteresting subtraces in the output
2014-05-19 wenzelm 2014-05-19 obsolete -- always pdf;
2014-05-19 wenzelm 2014-05-19 prefer T1 with searchable underscore (requires proper cm-super fonts);
2014-05-19 wenzelm 2014-05-19 merged
2014-05-19 wenzelm 2014-05-19 some adhoc event handling to unify L&F button focus behavior, e.g. Mac OS X vs. Nimbus;
2014-05-19 wenzelm 2014-05-19 re-focus target explicity, e.g. relevant for Sledgehammer panel;
2014-05-19 wenzelm 2014-05-19 clarified is_text in accordance to ML version (7e0178c84994), e.g. relevant for 'header' syntax in PIDE front-end;
2014-05-19 wenzelm 2014-05-19 more explicit identification for more robust adhoc change of environment /home/isatest/.isabelle/etc/settings -- notably for $ISABELLE_PLATFORM64;
2014-05-19 hoelzl 2014-05-19 renamed positive_integral to nn_integral
2014-05-19 blanchet 2014-05-19 hide more consts to beautify documentation
2014-05-19 hoelzl 2014-05-19 fixed document generation for HOL-Probability
2014-05-19 hoelzl 2014-05-19 introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
2014-05-19 desharna 2014-05-19 document property 'disc_map_iff'
2014-05-15 desharna 2014-05-15 generate 'disc_map_iff[simp]' theorem for (co)datatypes
2014-05-19 desharna 2014-05-19 fix 'set_empty' theorem when the discriminator is 'op ='
2014-05-18 nipkow 2014-05-18 typos
2014-05-18 wenzelm 2014-05-18 tuned comments;
2014-05-18 wenzelm 2014-05-18 clarified dependencies -- Mavericks presently does not work;
2014-05-18 wenzelm 2014-05-18 clarified docking layout, amending 9c2ca698690e;
2014-05-16 blanchet 2014-05-16 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
2014-05-16 blanchet 2014-05-16 removed needless transfer
2014-05-16 blanchet 2014-05-16 use 'simp add:' syntax in Sledgehammer rather than 'using'
2014-05-16 blanchet 2014-05-16 silence methods even better
2014-05-16 blanchet 2014-05-16 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
2014-05-16 wenzelm 2014-05-16 proper priority for error over warning, which got mixed up in 0546e036d1c0 and 4df2727a0b5f;