| Mon, 21 Dec 2020 15:13:49 +0100 |
step 4.6: two gaps in trace on SPARK
|
file | diff | annotate |
| Mon, 21 Dec 2020 11:55:10 +0100 |
step 4.5: separate trace for specific proof element
|
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 |
| Sun, 06 Apr 2014 16:36:28 +0200 |
more source positions;
|
file | diff | annotate |
| Mon, 31 Mar 2014 12:35:39 +0200 |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
file | diff | annotate |
| Sat, 01 Mar 2014 23:17:37 +0100 |
tuned signature;
|
file | diff | annotate |
| Sat, 01 Mar 2014 22:46:31 +0100 |
clarified language markup: added "delimited" property;
|
file | diff | annotate |
| Sun, 26 May 2013 20:42:43 +0200 |
tuned signature;
|
file | diff | annotate |
| Sat, 25 May 2013 15:37:53 +0200 |
syntax translations always depend on context;
|
file | diff | annotate |
| Thu, 04 Apr 2013 12:06:23 +0200 |
added var_position in analogy to longid_position, for typing reports on input;
|
file | diff | annotate |
| Fri, 29 Mar 2013 22:14:27 +0100 |
Pretty.item markup for improved readability of lists of items;
|
file | diff | annotate |
| Sun, 25 Nov 2012 19:49:24 +0100 |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file | diff | annotate |
| Mon, 01 Oct 2012 16:37:22 +0200 |
report sort assignment of visible type variables;
|
file | diff | annotate |
| Sat, 17 Mar 2012 13:06:23 +0100 |
added Syntax.read_typs;
|
file | diff | annotate |
| Fri, 09 Mar 2012 20:04:19 +0100 |
tuned signature;
|
file | diff | annotate |
| Fri, 17 Feb 2012 15:42:26 +0100 |
simplified configuration options for syntax ambiguity;
|
file | diff | annotate |
| Thu, 16 Feb 2012 22:18:28 +0100 |
simplified configuration options for syntax ambiguity;
|
file | diff | annotate |
| Wed, 15 Feb 2012 13:24:22 +0100 |
renamed "xstr" to "str_token";
|
file | diff | annotate |
| Mon, 16 Jan 2012 21:50:15 +0100 |
position constraints for numerals enable PIDE markup;
|
file | diff | annotate |
| Thu, 05 Jan 2012 20:26:01 +0100 |
discontinued Syntax.positions -- atomic parse trees are always annotated;
|
file | diff | annotate |
| Thu, 01 Dec 2011 12:25:27 +0100 |
renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
|
file | diff | annotate |
| Mon, 28 Nov 2011 22:05:32 +0100 |
separate module for concrete Isabelle markup;
|
file | diff | annotate |
| Fri, 25 Nov 2011 23:04:12 +0100 |
removed obsolete argument (cf. 954e9d6782ea);
|
file | diff | annotate |
| Fri, 25 Nov 2011 16:32:29 +0100 |
prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import;
|
file | diff | annotate |
| Mon, 14 Nov 2011 17:48:26 +0100 |
inner syntax positions for string literals;
|
file | diff | annotate |
| Wed, 09 Nov 2011 20:47:11 +0100 |
tuned signature;
|
file | diff | annotate |
| Wed, 09 Nov 2011 14:58:48 +0100 |
tuned signature -- emphasize internal role of these operations;
|
file | diff | annotate |
| Wed, 07 Sep 2011 21:05:53 +0200 |
explicit join_syntax ensures command transaction integrity of 'theory';
|
file | diff | annotate |
| Wed, 10 Aug 2011 16:05:14 +0200 |
future_job: explicit indication of interrupts;
|
file | diff | annotate |
| Sat, 06 Aug 2011 15:48:08 +0200 |
make syntax ambiguity warnings a config option
|
file | diff | annotate |
| Sun, 10 Jul 2011 20:59:04 +0200 |
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
|
file | diff | annotate |
| Mon, 27 Jun 2011 15:01:08 +0200 |
parallel Syntax.parse, which is rather slow;
|
file | diff | annotate |
| Sun, 15 May 2011 22:22:26 +0200 |
future merge of grammars, to improve parallel performance;
|
file | diff | annotate |
| Tue, 26 Apr 2011 21:05:52 +0200 |
clarified auxiliary structure Lexicon.Syntax;
|
file | diff | annotate |
| Tue, 19 Apr 2011 21:55:42 +0200 |
explicit markup for loose bounds;
|
file | diff | annotate |
| Tue, 19 Apr 2011 15:58:05 +0200 |
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
|
file | diff | annotate |
| Tue, 19 Apr 2011 14:57:09 +0200 |
simplified check/uncheck interfaces: result comparison is hardwired by default;
|
file | diff | annotate |
| Mon, 18 Apr 2011 11:13:29 +0200 |
simplified pretty printing context, which is only required for certain kernel operations;
|
file | diff | annotate |
| Sun, 17 Apr 2011 23:47:05 +0200 |
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
|
file | diff | annotate |
| Sat, 16 Apr 2011 15:47:52 +0200 |
modernized structure Proof_Context;
|
file | diff | annotate |
| Fri, 08 Apr 2011 22:40:29 +0200 |
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
|
file | diff | annotate |
| Fri, 08 Apr 2011 21:11:29 +0200 |
discontinued Syntax.max_pri, which is not really a symbolic parameter;
|
file | diff | annotate |
| Fri, 08 Apr 2011 18:08:13 +0200 |
simplified Pure syntax bootstrap;
|
file | diff | annotate |
| Fri, 08 Apr 2011 17:45:37 +0200 |
renamed sprop "prop#" to "prop'" -- proper identifier;
|
file | diff | annotate |
| Fri, 08 Apr 2011 16:34:14 +0200 |
discontinued special treatment of structure Lexicon;
|
file | diff | annotate |
| Fri, 08 Apr 2011 15:48:14 +0200 |
discontinued special status of structure Printer;
|
file | diff | annotate |
| Fri, 08 Apr 2011 15:02:11 +0200 |
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
|
file | diff | annotate |
| Fri, 08 Apr 2011 14:20:57 +0200 |
discontinued special treatment of structure Mixfix;
|
file | diff | annotate |
| Fri, 08 Apr 2011 13:31:16 +0200 |
explicit structure Syntax_Trans;
|
file | diff | annotate |
| Thu, 07 Apr 2011 21:37:42 +0200 |
tuned signature;
|
file | diff | annotate |
| Thu, 07 Apr 2011 18:24:59 +0200 |
discontinued user-defined token translations;
|
file | diff | annotate |
| Wed, 06 Apr 2011 23:04:00 +0200 |
separate structure Term_Position;
|
file | diff | annotate |
| Wed, 06 Apr 2011 22:25:44 +0200 |
type syntax as regular mixfix specification (type_ext for bootstrapping has been obsolete for many years);
|
file | diff | annotate |
| Wed, 06 Apr 2011 17:15:06 +0200 |
eliminated slightly odd Syntax.rep_syntax;
|
file | diff | annotate |
| Wed, 06 Apr 2011 17:00:40 +0200 |
more abstract print translation;
|
file | diff | annotate |
| Wed, 06 Apr 2011 16:15:57 +0200 |
more abstract syntax translation;
|
file | diff | annotate |