2015-07-21 wenzelm 2015-07-21 support for ML debugger;
2015-07-21 wenzelm 2015-07-21 more explicit thread identification;
2015-07-21 wenzelm 2015-07-21 avoid lxbroy2, lxbroy3, lxbroy4, which are often busy with other processes;
2015-07-20 paulson 2015-07-20 new material for multivariate analysis, etc.
2015-07-20 wenzelm 2015-07-20 proper LaTeX;
2015-07-19 wenzelm 2015-07-19 updated to jdk-8u51;
2015-07-19 wenzelm 2015-07-19 more symbols;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-07-18 wenzelm 2015-07-18 merged
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-07-18 wenzelm 2015-07-18 tuned whitespace;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-07-18 wenzelm 2015-07-18 reactivated dead code;
2015-07-17 wenzelm 2015-07-17 more uniform ComponentAdapter;
2015-07-17 wenzelm 2015-07-17 skeleton for interactive debugger;
2015-07-17 wenzelm 2015-07-17 tuned;
2015-07-17 wenzelm 2015-07-17 tuned;
2015-07-17 wenzelm 2015-07-17 store breakpoints within ML environment;
2015-07-17 wenzelm 2015-07-17 clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default; tuned;
2015-07-17 wenzelm 2015-07-17 report possible breakpoint positions;
2015-07-17 wenzelm 2015-07-17 proper attribute;
2015-07-17 traytel 2015-07-17 forgotten selector
2015-07-16 blanchet 2015-07-16 made code less loopy
2015-07-16 blanchet 2015-07-16 keep smart default for Isar proofs in Sledgehammer panel (if the option is not checked)
2015-07-16 blanchet 2015-07-16 generalized generic translation function
2015-07-16 blanchet 2015-07-16 merge
2015-07-16 blanchet 2015-07-16 tuning
2015-07-16 blanchet 2015-07-16 generalized limitation in documentation
2015-07-16 blanchet 2015-07-16 made tactic more robust w.r.t. equations containing 'case_prod'
2015-07-16 wenzelm 2015-07-16 merged
2015-07-16 wenzelm 2015-07-16 merged
2015-07-16 wenzelm 2015-07-16 clarified boundary cases of completion;
2015-07-16 wenzelm 2015-07-16 additional ML parse tree components for Poly/ML 5.5.3, or later; support for ML completion; tuned;
2015-07-16 wenzelm 2015-07-16 added option ML_debugger;
2015-07-16 wenzelm 2015-07-16 ML debugger interface;
2015-07-16 traytel 2015-07-16 {r,e,d,f}tac with proper context in BNF
2015-07-16 hoelzl 2015-07-16 move disjoint sets to their own theory
2015-07-15 wenzelm 2015-07-15 back to uniform BUILD_ARGS: first some options, then some sessions (cf. 4fce5d462afc);
2015-07-14 wenzelm 2015-07-14 merged
2015-07-14 wenzelm 2015-07-14 more explicit command-line option for isabelle build;
2015-07-14 wenzelm 2015-07-14 more aggressive compaction of multi-goal proof terms (see also a8babbb6d5ea, 4dd0ba632e40);
2015-07-14 wenzelm 2015-07-14 normalize proof before splitting conjunctions, according to Proof.conclude_goal (see also 4dd0ba632e40) -- may reduce general resource usage;
2015-07-14 hoelzl 2015-07-14 generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal
2015-07-14 hoelzl 2015-07-14 add continuous_onI_mono
2015-07-13 blanchet 2015-07-13 tuned description
2015-07-13 blanchet 2015-07-13 tuning
2015-07-13 blanchet 2015-07-13 updated Isabelle description to CASC
2015-07-13 blanchet 2015-07-13 imported patch up_casc
2015-07-13 hoelzl 2015-07-13 add emeasure_add_AE
2015-07-13 hoelzl 2015-07-13 stronger induction assumption in lfp_transfer and emeasure_lfp
2015-07-13 wenzelm 2015-07-13 refrain from testing HOL-Proofs for x86_64-linux: takes more than 4h; tuned parameters;
2015-07-12 Lars Hupel 2015-07-12 Quickcheck setup for finite sets
2015-07-11 wenzelm 2015-07-11 tuned proofs;
2015-07-11 wenzelm 2015-07-11 tuned proofs;
2015-07-09 wenzelm 2015-07-09 merged
2015-07-09 wenzelm 2015-07-09 tuned proofs;
2015-07-09 wenzelm 2015-07-09 SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
2015-07-09 wenzelm 2015-07-09 clarified specific use of inspect_contract: "any Bound variable will do" may render the term invalid for Term.fastype_of1 in inst_subst_tac (see also 7c3757fccf0e);