2013-01-31 hoelzl 2013-01-31 use order topology for extended reals
2013-01-31 hoelzl 2013-01-31 introduce order topology
2013-01-31 hoelzl 2013-01-31 simplify heine_borel type class
2013-01-31 blanchet 2013-01-31 compute proper weight for "p proves p" in MaSh
2013-01-15 kuncar 2013-01-15 restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
2013-01-25 nipkow 2013-01-25 tuned
2013-01-20 wenzelm 2013-01-20 back to post-release mode -- after fork point;
2013-01-20 wenzelm 2013-01-20 updated for release;
2013-01-20 wenzelm 2013-01-20 merged
2013-01-20 wenzelm 2013-01-20 misc tuning for release;
2013-01-20 wenzelm 2013-01-20 tuned;
2013-01-20 wenzelm 2013-01-20 accomodate scala-2.9.2;
2013-01-19 wenzelm 2013-01-19 afford parallel proof terms;
2013-01-19 wenzelm 2013-01-19 always close derivation at the bottom of forked proofs (despite increased non-determinism of proof terms) -- improve parallel performance by avoiding dynamic dependency within large Isar proofs, e.g. Slicing/JinjaVM/SemanticsWF.thy in AFP/bf9b14cbc707;
2013-01-19 nipkow 2013-01-19 simplified proofs
2013-01-19 blanchet 2013-01-19 tuning
2013-01-19 wenzelm 2013-01-19 misc cleanup;
2013-01-19 wenzelm 2013-01-19 tuned signature;
2013-01-18 wenzelm 2013-01-18 use inlined session name as title for charts; tuned signature;
2013-01-18 wenzelm 2013-01-18 tuned signature;
2013-01-18 wenzelm 2013-01-18 charts for future task runtime statistics;
2013-01-18 wenzelm 2013-01-18 merged
2013-01-18 wenzelm 2013-01-18 more uniform permissions;
2013-01-18 wenzelm 2013-01-18 more generous C stack size as in Linux and Mac OS X, to reduce chance of Cygwin-specific crashes; more generous initial C heap within VM; proper executable;
2013-01-18 wenzelm 2013-01-18 tuned proof -- much faster;
2013-01-18 wenzelm 2013-01-18 more systematic task statistics;
2013-01-18 wenzelm 2013-01-18 added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);
2013-01-18 hoelzl 2013-01-18 generalized diameter from real_normed_vector to metric_space
2013-01-18 hoelzl 2013-01-18 tuned proof
2013-01-18 hoelzl 2013-01-18 tune prove compact_eq_totally_bounded
2013-01-17 huffman 2013-01-17 generalized theorem edelstein_fix to class metric_space
2013-01-18 blanchet 2013-01-18 tuning
2013-01-18 blanchet 2013-01-18 pass correct index to "Sign.typ_unify" -- this is important to avoid what appears to be an infinite loop in the unifier
2013-01-18 blanchet 2013-01-18 optimization -- evaluate conversion to table only once
2013-01-17 blanchet 2013-01-17 MeSh prover generation
2013-01-17 blanchet 2013-01-17 use correct weights in MeSh driver
2013-01-17 blanchet 2013-01-17 use precomputed MaSh/MePo data whenever available
2013-01-17 wenzelm 2013-01-17 merged
2013-01-17 wenzelm 2013-01-17 merged
2013-01-17 wenzelm 2013-01-17 copy Cygwin-Latex-Setup.bat;
2013-01-17 wenzelm 2013-01-17 more formal Cygwin-Latex-Setup (excluding bulky texlive-collection-fontsextra, which would be required for eulervm.sty);
2013-01-17 wenzelm 2013-01-17 updated to cygwin-20130117;
2013-01-17 wenzelm 2013-01-17 proper permissions;
2013-01-17 wenzelm 2013-01-17 tuned;
2013-01-17 wenzelm 2013-01-17 updated to jdk-7u11;
2013-01-17 huffman 2013-01-17 simplify proof of compact_imp_bounded
2013-01-17 blanchet 2013-01-17 added step to skip some queries
2013-01-17 blanchet 2013-01-17 provide a means to skip a method
2013-01-17 blanchet 2013-01-17 evaluate more cases (cf. paper)
2013-01-17 blanchet 2013-01-17 updated MaSh
2013-01-17 blanchet 2013-01-17 make SPASS more configurable, for experiments
2013-01-15 huffman 2013-01-15 generalize more topology lemmas
2013-01-15 huffman 2013-01-15 generalize topology lemmas; simplify proofs
2013-01-17 wenzelm 2013-01-17 merged
2013-01-17 wenzelm 2013-01-17 tuned signature (again) -- keep Properties more generic;
2013-01-17 wenzelm 2013-01-17 tuned proofs;
2013-01-17 hoelzl 2013-01-17 simplified prove of compact_imp_bounded
2013-01-17 hoelzl 2013-01-17 use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma
2013-01-17 hoelzl 2013-01-17 move auxiliary lemma to top
2013-01-17 hoelzl 2013-01-17 add countable compacteness; replace finite_range_imp_infinite_repeats by pigeonhole_infinite