2015-07-25 wenzelm 2015-07-25 more accurate maxidx;
2015-07-25 wenzelm 2015-07-25 clarified error;
2015-07-25 wenzelm 2015-07-25 added infer_instantiate, which is meant to supersede cterm_instantiate;
2015-07-24 wenzelm 2015-07-24 eliminated alias;
2015-07-24 wenzelm 2015-07-24 proper context;
2015-07-24 wenzelm 2015-07-24 unused;
2015-07-24 wenzelm 2015-07-24 proper context;
2015-07-23 wenzelm 2015-07-23 more symbols by default, without xsymbols mode;
2015-07-23 hoelzl 2015-07-23 Measures form a CCPO
2015-07-23 hoelzl 2015-07-23 reorganized Extended_Real
2015-07-23 wenzelm 2015-07-23 isabelle update_cartouches;
2015-07-23 wenzelm 2015-07-23 tuned proofs;
2015-07-23 wenzelm 2015-07-23 proper latex;
2015-07-22 wenzelm 2015-07-22 tuned proofs;
2015-07-22 wenzelm 2015-07-22 tuned proofs;
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