| Tue, 22 Oct 2024 12:03:46 +0200 |
wenzelm |
clarified markers for syntax consts: avoid overlap with logical consts;
|
file |
diff |
annotate
|
| Fri, 18 Oct 2024 14:20:09 +0200 |
wenzelm |
more inner-syntax markup;
|
file |
diff |
annotate
|
| Tue, 08 Oct 2024 12:10:35 +0200 |
wenzelm |
more inner-syntax markup;
|
file |
diff |
annotate
|
| Sun, 06 Oct 2024 22:56:07 +0200 |
wenzelm |
more inner-syntax markup, without pretty blocks;
|
file |
diff |
annotate
|
| Sun, 22 Sep 2024 15:58:55 +0200 |
wenzelm |
clarified inner syntax markup: use "notation" uniformly;
|
file |
diff |
annotate
|
| Fri, 20 Sep 2024 23:36:33 +0200 |
wenzelm |
more inner syntax markup: Pure;
|
file |
diff |
annotate
|
| Tue, 17 Sep 2024 17:51:55 +0200 |
wenzelm |
more explicit context for syn_ext/mixfix operations, but it often degenerates to background theory;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2024 22:47:51 +0200 |
wenzelm |
more markup for syntax consts;
|
file |
diff |
annotate
|
| Fri, 22 Dec 2023 21:03:16 +0100 |
wenzelm |
clarified signature: downgrade old-style Global_Theory.add_defs to Global_Theory.add_def without attributes;
|
file |
diff |
annotate
|
| Mon, 04 Dec 2023 12:10:39 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Tue, 21 Sep 2021 12:25:40 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2021 20:22:32 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2020 14:56:55 +0200 |
wenzelm |
prefer conservative extend/merge of theory naming;
|
file |
diff |
annotate
|
| Tue, 21 Apr 2020 22:19:59 +0200 |
wenzelm |
clarified signature: avoid clash with Isabelle/Scala Term.OFCLASS on case-insensible file-system;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2020 16:12:50 +0100 |
wenzelm |
some uses of "' " as witness for this feature;
|
file |
diff |
annotate
|
| Sat, 23 Nov 2019 14:48:44 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 24 Jul 2019 10:49:01 +0200 |
wenzelm |
avoid global syntax for MinProof (amending e31271559de8);
|
file |
diff |
annotate
|
| Sun, 21 Jul 2019 15:19:07 +0200 |
wenzelm |
global declaration of abstract syntax for proof terms, with qualified names;
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 15:44:46 +0100 |
wenzelm |
eliminated ASCII syntax from Pure bootstrap;
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 12:59:08 +0100 |
wenzelm |
notation for dummy sort;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Thu, 04 Aug 2016 21:30:20 +0200 |
wenzelm |
prefer hardwired "nothing";
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 16:15:31 +0200 |
wenzelm |
explicit property for unbreakable block;
|
file |
diff |
annotate
|
| Wed, 30 Mar 2016 15:15:12 +0200 |
wenzelm |
clarified simple mixfix;
|
file |
diff |
annotate
|
| Tue, 29 Mar 2016 21:17:29 +0200 |
wenzelm |
more position information for type mixfix;
|
file |
diff |
annotate
|
| Sun, 06 Mar 2016 16:19:02 +0100 |
wenzelm |
clarified treatment of fragments of Isabelle symbols during bootstrap;
|
file |
diff |
annotate
|
| Sat, 09 Jan 2016 12:35:07 +0100 |
wenzelm |
discontinued \<struct> syntax;
|
file |
diff |
annotate
|
| Tue, 29 Dec 2015 14:58:15 +0100 |
wenzelm |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 22:42:48 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 22:38:22 +0200 |
wenzelm |
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 14:32:23 +0200 |
wenzelm |
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
|
file |
diff |
annotate
|
| Wed, 09 Sep 2015 14:47:41 +0200 |
wenzelm |
eliminated \<Colon> from syntax of constraints;
|
file |
diff |
annotate
|
| Mon, 22 Sep 2014 21:28:57 +0200 |
wenzelm |
discontinued old "xnum" token category;
|
file |
diff |
annotate
|
| Sun, 06 Apr 2014 15:43:45 +0200 |
wenzelm |
more source positions;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 15:12:03 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 12:34:50 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 11:42:32 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 11:06:39 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 10:45:03 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 20 Mar 2014 22:40:12 +0100 |
wenzelm |
produce qualified names more directly;
|
file |
diff |
annotate
|
| Wed, 22 Jan 2014 15:10:33 +0100 |
wenzelm |
inner syntax token language allows regular quoted strings;
|
file |
diff |
annotate
|
| Sat, 18 Jan 2014 19:15:12 +0100 |
wenzelm |
support for nested text cartouches;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 20:35:50 +0200 |
wenzelm |
added Theory.setup convenience;
|
file |
diff |
annotate
|
| Tue, 28 May 2013 23:06:32 +0200 |
wenzelm |
explicit support for type annotations within printed syntax trees;
|
file |
diff |
annotate
|
| Sun, 26 May 2013 21:05:03 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 26 May 2013 20:42:43 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| Thu, 04 Apr 2013 12:06:23 +0200 |
wenzelm |
added var_position in analogy to longid_position, for typing reports on input;
|
file |
diff |
annotate
|
| Sun, 30 Dec 2012 16:23:30 +0100 |
wenzelm |
uniform notation for == and \<equiv> (cf. 3e3c2af5e8a5);
|
file |
diff |
annotate
|
| Wed, 19 Dec 2012 22:26:26 +0100 |
nipkow |
removed odd associativity of ==
|
file |
diff |
annotate
|
| Wed, 03 Oct 2012 14:58:56 +0200 |
wenzelm |
allow position constraints to coexist with 0 or 1 sort constraints;
|
file |
diff |
annotate
|
| Mon, 01 Oct 2012 16:37:22 +0200 |
wenzelm |
report sort assignment of visible type variables;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 13:24:22 +0100 |
wenzelm |
renamed "xstr" to "str_token";
|
file |
diff |
annotate
|
| Mon, 16 Jan 2012 21:50:15 +0100 |
wenzelm |
position constraints for numerals enable PIDE markup;
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 12:25:27 +0100 |
wenzelm |
renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
|
file |
diff |
annotate
|
| Mon, 14 Nov 2011 17:48:26 +0100 |
wenzelm |
inner syntax positions for string literals;
|
file |
diff |
annotate
|
| Mon, 07 Nov 2011 16:41:16 +0100 |
wenzelm |
discontinued numbered structure indexes (legacy feature);
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 23:39:05 +0200 |
wenzelm |
special treatment of structure index 1 in Pure, including legacy warning;
|
file |
diff |
annotate
|