2016-04-02 ago prefer infix operations;
2016-04-02 ago careful export of type-dependent functions, without losing their special status;
2016-03-18 ago clarified modules;
2016-03-03 ago clarified modules;
2016-01-24 ago tuned;
2015-12-21 ago discontinued built-in profiling: avoid danger of conflicting invocations (multithreading etc.);
2015-09-21 ago separate panel for proof state output;
2015-08-11 ago default ML context for all command transactions, e.g. relevant for debugging and toplevel pretty-printing;
2015-07-08 ago more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
2015-06-09 ago tuned signature;
2015-05-03 ago tuned output;
2015-04-22 ago allow diagnostic proof commands with skip_proofs;
2015-04-22 ago tuned signature;
2015-04-16 ago discontinued pointless warnings: commands are only defined inside a theory context;
2015-04-16 ago explicit error for Toplevel.proof_of;
2015-04-15 ago tuned messages;
2015-04-09 ago clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
2015-04-06 ago support for 'restricted' modifier: only qualified accesses outside the local scope;
2015-04-04 ago support private scope for individual local theory commands;
2015-01-29 ago discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
2014-12-23 ago explicit message channels for "state", "information";
2014-12-19 ago tuned;
2014-11-26 ago more informative failure of protocol commands, with exception trace;
2014-11-22 ago tuned;
2014-11-13 ago uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
2014-11-06 ago more explicit Keyword.keywords;
2014-11-03 ago eliminated unused int_only flag (see also c12484a27367);
2014-10-31 ago discontinued pointless option: timing is always on (overall theory only);
2014-10-31 ago eliminated odd flags and hook;
2014-10-28 ago 'oops' requires proper goal statement -- exclude 'notepad' to avoid disrupting begin/end structure;
2014-10-28 ago tuned;
2014-07-02 ago centralized (ad-hoc) switching of targets in named_target.ML
2014-06-07 ago avoid odd Named_Target.reinit altogether
2014-06-07 ago clarified terminology: toplevel is interwined with named targets in particular, not with local theories in general
2014-05-12 ago smarter recovery from toplevel type error;
2014-05-07 ago print results as "state", to avoid intrusion into the source text;
2014-05-07 ago discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
2014-05-07 ago tuned;
2014-05-06 ago clarified print_state, which goes back to TTY loop before Proof General, and before separate print_context;
2014-05-05 ago more print operations;
2014-03-31 ago some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-27 ago clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-24 ago discontinued Toplevel.debug in favour of system option "exception_trace";
2014-03-14 ago prefer more robust Synchronized.var;
2014-03-12 ago more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges;
2014-03-11 ago slightly more rubust (and opportunistic) exit for old-fashioned theory_to_proof, which is used by global 'sublocale' with Named_Target.init but without proper exit;
2014-02-13 ago tuned whitespace;
2013-12-05 ago more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
2013-11-11 ago tuned signature;
2013-09-18 ago improved printing of exception trace in Poly/ML 5.5.1;
2013-09-04 ago some explicit indication of Proof General legacy;
2013-08-25 ago maintain goal forks as part of global execution;
2013-08-25 ago discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
2013-07-30 ago type theory is purely value-oriented;
2013-07-18 ago immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
2013-07-09 ago tuned message;
2013-07-05 ago tuned signature;
2013-07-04 ago separate exec_id assignment for Command.print states, without affecting result of eval;
2013-07-02 ago clarified Proofterm.proofs vs. Goal.skip_proofs;
2013-05-22 ago mark local theory as brittle also after interpretation inside locales;