| Fri, 11 Dec 2020 18:34:10 +0100 |
step 3.4+: where in src/Pure can @{print} be used
|
file | diff | annotate |
| Wed, 23 Sep 2020 15:18:07 +0200 |
\----- start update Isabelle2019 --> Isabelle2020
|
file | diff | annotate |
| Tue, 03 Sep 2019 16:10:31 +0200 |
\----- start update Isabelle2018 --> Isabelle2019
|
file | diff | annotate |
| Wed, 22 Aug 2018 14:44:15 +0200 |
\----- start update Isabelle2017 --> Isabelle2018
|
file | diff | annotate |
| Fri, 19 Jan 2018 12:49:17 +0100 |
\----- start update Isabelle2015 --> Isabelle2017
|
file | diff | annotate |
| Sat, 05 Dec 2015 16:09:41 +0100 |
switched from Isabelle2014 to Isabelle2015, intermediate state
|
file | diff | annotate |
| Fri, 08 May 2015 12:57:56 +0200 |
separate isabisac form Isabelle2014
|
file | diff | annotate |
| Mon, 20 Apr 2015 14:18:40 +0200 |
update test/ to Isabelle2014 (~ updates of src/)
|
file | diff | annotate |
| Tue, 14 Apr 2015 13:41:48 +0200 |
build session Isac starts in Isabelle2014
|
file | diff | annotate |
| Thu, 24 Jul 2014 15:54:56 +0200 |
further distinction of Isabelle distribution: alert for identified release candidates;
|
file | diff | annotate |
| Sun, 06 Apr 2014 16:36:28 +0200 |
more source positions;
|
file | diff | annotate |
| Sun, 06 Apr 2014 15:19:22 +0200 |
clarified ML bootstrap;
|
file | diff | annotate |
| Thu, 27 Mar 2014 17:12:40 +0100 |
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
|
file | diff | annotate |
| Wed, 26 Mar 2014 09:19:04 +0100 |
tuned comments;
|
file | diff | annotate |
| Wed, 26 Mar 2014 09:13:38 +0100 |
tuned load order;
|
file | diff | annotate |
| Tue, 25 Mar 2014 19:03:02 +0100 |
proper configuration option "ML_print_depth";
|
file | diff | annotate |
| Thu, 20 Mar 2014 19:24:51 +0100 |
tuned error, according to "use" in General/secure.ML;
|
file | diff | annotate |
| Tue, 18 Mar 2014 18:09:31 +0100 |
clarified module arrangement;
|
file | diff | annotate |
| Tue, 18 Mar 2014 17:39:03 +0100 |
clarifed module name;
|
file | diff | annotate |
| Tue, 18 Mar 2014 16:44:51 +0100 |
clarified module arrangement;
|
file | diff | annotate |
| Tue, 18 Mar 2014 16:16:28 +0100 |
clarified modules;
|
file | diff | annotate |
| Tue, 18 Mar 2014 13:36:28 +0100 |
clarified bootstrap process: switch to ML with context and antiquotations earlier;
|
file | diff | annotate |
| Wed, 12 Mar 2014 22:57:50 +0100 |
tuned signature -- clarified module name;
|
file | diff | annotate |
| Tue, 11 Mar 2014 18:26:47 +0100 |
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
|
file | diff | annotate |
| Sat, 22 Feb 2014 20:52:43 +0100 |
support for completion within the formal context;
|
file | diff | annotate |
| Sun, 16 Feb 2014 17:25:03 +0100 |
prefer user-space tool within Pure.thy;
|
file | diff | annotate |
| Mon, 10 Feb 2014 22:39:04 +0100 |
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
|
file | diff | annotate |
| Sat, 25 Jan 2014 18:34:05 +0100 |
prefer self-contained user-space tool;
|
file | diff | annotate |
| Fri, 17 Jan 2014 20:31:39 +0100 |
prefer user-space tool within Pure.thy;
|
file | diff | annotate |
| Fri, 13 Dec 2013 20:20:15 +0100 |
maintain morphism names for diagnostic purposes;
|
file | diff | annotate |
| Wed, 11 Dec 2013 18:02:22 +0100 |
support for polml-5.5.2;
|
file | diff | annotate |
| Sat, 16 Nov 2013 17:39:11 +0100 |
toplevel function "use" refers to raw ML bootstrap environment;
|
file | diff | annotate |
| Wed, 18 Sep 2013 13:31:44 +0200 |
updated to polyml-5.5.1;
|
file | diff | annotate |
| Wed, 18 Sep 2013 13:18:51 +0200 |
improved printing of exception trace in Poly/ML 5.5.1;
|
file | diff | annotate |
| Wed, 18 Sep 2013 11:08:28 +0200 |
moved module into plain Isabelle/ML user space;
|
file | diff | annotate |
| Mon, 26 Aug 2013 21:56:08 +0200 |
added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
|
file | diff | annotate |
| Sun, 25 Aug 2013 20:32:26 +0200 |
maintain goal forks as part of global execution;
|
file | diff | annotate |
| Thu, 08 Aug 2013 23:52:35 +0200 |
removed unused YXML_Find_Theorems and Legacy_XML_Syntax;
|
file | diff | annotate |
| Mon, 05 Aug 2013 17:14:02 +0200 |
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
|
file | diff | annotate |
| Thu, 01 Aug 2013 22:47:52 +0200 |
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
|
file | diff | annotate |
| Tue, 30 Jul 2013 18:19:16 +0200 |
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
|
file | diff | annotate |
| Tue, 30 Jul 2013 15:09:25 +0200 |
type theory is purely value-oriented;
|
file | diff | annotate |
| Fri, 12 Jul 2013 11:07:02 +0200 |
clarified module name;
|
file | diff | annotate |
| Thu, 11 Jul 2013 14:42:11 +0200 |
global management of command execution fragments;
|
file | diff | annotate |
| Wed, 10 Jul 2013 23:25:28 +0200 |
more abstract message channel;
|
file | diff | annotate |
| Fri, 05 Jul 2013 23:10:18 +0200 |
more uniform Counter in ML and Scala;
|
file | diff | annotate |
| Fri, 05 Jul 2013 22:58:24 +0200 |
tuned signature;
|
file | diff | annotate |
| Fri, 05 Jul 2013 15:38:03 +0200 |
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
|
file | diff | annotate |
| Wed, 03 Jul 2013 16:58:35 +0200 |
tuned signature;
|
file | diff | annotate |
| Sun, 30 Jun 2013 11:37:34 +0200 |
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
|
file | diff | annotate |
| Thu, 27 Jun 2013 23:17:26 +0200 |
manage option "proofs" within theory context -- with minor overhead for primitive inferences;
|
file | diff | annotate |
| Tue, 28 May 2013 23:06:32 +0200 |
explicit support for type annotations within printed syntax trees;
|
file | diff | annotate |
| Sat, 25 May 2013 15:44:08 +0200 |
tuned structure
|
file | diff | annotate |
| Fri, 17 May 2013 20:41:45 +0200 |
proper option quick_and_dirty;
|
file | diff | annotate |
| Fri, 17 May 2013 17:11:06 +0200 |
event timer as separate service thread;
|
file | diff | annotate |
| Wed, 15 May 2013 20:34:42 +0200 |
moved files;
|
file | diff | annotate |
| Wed, 15 May 2013 20:22:46 +0200 |
maintain ProofGeneral preferences within ProofGeneral module;
|
file | diff | annotate |
| Wed, 15 May 2013 17:39:41 +0200 |
just one ProofGeneral module;
|
file | diff | annotate |
| Tue, 14 May 2013 21:56:19 +0200 |
simplified modules and exceptions;
|
file | diff | annotate |
| Mon, 13 May 2013 21:42:27 +0200 |
more direct output of remaining PGIP rudiments;
|
file | diff | annotate |