2014-12-30 wenzelm 2014-12-30 explicit message channel for "legacy", which is nonetheless a variant of "warning";
2014-12-29 wenzelm 2014-12-29 more toplevel pretty printing;
2014-12-22 wenzelm 2014-12-22 separate module Random; proper Synchronized.var;
2014-12-03 wenzelm 2014-12-03 node-specific keywords, with session base syntax as default;
2014-11-30 wenzelm 2014-11-30 more abstract type Input.source;
2014-11-26 wenzelm 2014-11-26 load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
2014-11-21 wenzelm 2014-11-21 removed some add-ons from modules that are relevant for the inference kernel;
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.keywords; tuned signature;
2014-10-31 wenzelm 2014-10-31 discontinued Isar TTY loop;
2014-10-31 wenzelm 2014-10-31 discontinued Proof General;
2014-10-13 wenzelm 2014-10-13 obsolete;
2014-10-13 wenzelm 2014-10-13 clarified load order; tuned signature;
2014-09-29 wenzelm 2014-09-29 pro-forma support for polyml-5.5.3 (presently SVN 1960);
2014-08-22 wenzelm 2014-08-22 clarified ML toplevel pp: avoid ML output to be attached to inlined binding positions;
2014-08-19 wenzelm 2014-08-19 clarified modules;
2014-08-14 wenzelm 2014-08-14 tuned signature -- prefer self-contained user-space tool;
2014-08-13 wenzelm 2014-08-13 load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;
2014-08-12 wenzelm 2014-08-12 separate module Command_Span: mostly syntactic representation; potentially prover-specific Output_Syntax.parse_spans;
2014-07-24 wenzelm 2014-07-24 further distinction of Isabelle distribution: alert for identified release candidates;
2014-04-06 wenzelm 2014-04-06 more source positions;
2014-04-06 wenzelm 2014-04-06 clarified ML bootstrap;
2014-03-27 wenzelm 2014-03-27 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
2014-03-26 wenzelm 2014-03-26 tuned comments;
2014-03-26 wenzelm 2014-03-26 tuned load order;
2014-03-25 wenzelm 2014-03-25 proper configuration option "ML_print_depth"; proper ML_exception_trace for HOL-TPTP;
2014-03-20 wenzelm 2014-03-20 tuned error, according to "use" in General/secure.ML;
2014-03-18 wenzelm 2014-03-18 clarified module arrangement;
2014-03-18 wenzelm 2014-03-18 clarifed module name;
2014-03-18 wenzelm 2014-03-18 clarified module arrangement; more antiquotations;
2014-03-18 wenzelm 2014-03-18 clarified modules; more antiquotations for antiquotations;
2014-03-18 wenzelm 2014-03-18 clarified bootstrap process: switch to ML with context and antiquotations earlier;
2014-03-12 wenzelm 2014-03-12 tuned signature -- clarified module name;
2014-03-11 wenzelm 2014-03-11 tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
2014-02-22 wenzelm 2014-02-22 support for completion within the formal context; tuned signature;
2014-02-16 wenzelm 2014-02-16 prefer user-space tool within Pure.thy;
2014-02-10 wenzelm 2014-02-10 seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
2014-01-25 wenzelm 2014-01-25 prefer self-contained user-space tool;
2014-01-17 wenzelm 2014-01-17 prefer user-space tool within Pure.thy;
2013-12-13 wenzelm 2013-12-13 maintain morphism names for diagnostic purposes;
2013-12-11 wenzelm 2013-12-11 support for polml-5.5.2; support Thread.numPhysicalProcessors of polyml-5.5.2 (according to SVN 1890); clarified max_threads: store plain value internally, reproduce result only on startup, and thus avoid potential system overhead;
2013-11-16 wenzelm 2013-11-16 toplevel function "use" refers to raw ML bootstrap environment;
2013-09-18 wenzelm 2013-09-18 updated to polyml-5.5.1;
2013-09-18 wenzelm 2013-09-18 improved printing of exception trace in Poly/ML 5.5.1;
2013-09-18 wenzelm 2013-09-18 moved module into plain Isabelle/ML user space;
2013-08-26 wenzelm 2013-08-26 added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
2013-08-25 wenzelm 2013-08-25 maintain goal forks as part of global execution; tuned;
2013-08-08 wenzelm 2013-08-08 removed unused YXML_Find_Theorems and Legacy_XML_Syntax;
2013-08-05 wenzelm 2013-08-05 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
2013-08-01 wenzelm 2013-08-01 exception trace for Poly/ML 5.5.1, using regular Isabelle output;
2013-07-30 wenzelm 2013-07-30 recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2013-07-12 wenzelm 2013-07-12 clarified module name;
2013-07-11 wenzelm 2013-07-11 global management of command execution fragments; tuned;
2013-07-10 wenzelm 2013-07-10 more abstract message channel;
2013-07-05 wenzelm 2013-07-05 more uniform Counter in ML and Scala;
2013-07-05 wenzelm 2013-07-05 tuned signature; tuned comments;
2013-07-05 wenzelm 2013-07-05 explicit module Document_ID as source of globally unique identifiers across ML/Scala;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2013-06-30 wenzelm 2013-06-30 backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;