| Thu, 28 Oct 2021 18:37:33 +0200 |
wenzelm |
support for "lemma";
|
file |
diff |
annotate
|
| Thu, 28 Oct 2021 13:13:48 +0200 |
wenzelm |
local fixes for "lemma" antiquotation;
|
file |
diff |
annotate
|
| Thu, 28 Oct 2021 12:25:47 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 28 Oct 2021 12:14:53 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 28 Oct 2021 12:09:58 +0200 |
wenzelm |
clarified keywords: major take precedence for commands, but not used for antiquotations;
|
file |
diff |
annotate
|
| Tue, 26 Oct 2021 22:26:47 +0200 |
wenzelm |
tuned, continuing e955964d89cb;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 20:25:33 +0200 |
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
|
| Fri, 09 Apr 2021 21:07:11 +0200 |
wenzelm |
clarified signature: more detailed token positions for antiquotations;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2020 15:08:56 +0200 |
wenzelm |
tuned -- avoid non-standard extend/merge;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|
| Fri, 23 Feb 2018 21:27:20 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 18:59:33 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Mon, 12 Jun 2017 11:32:23 +0200 |
wenzelm |
more markup for HTML rendering;
|
file |
diff |
annotate
|
| Mon, 23 May 2016 21:30:30 +0200 |
wenzelm |
embedded content may be delimited via cartouches;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 13:54:02 +0200 |
wenzelm |
simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 20:03:24 +0200 |
wenzelm |
clarified modules -- simplified bootstrap;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 16:36:26 +0100 |
wenzelm |
clarified type Token.src: plain token list, with usual implicit value assignment;
|
file |
diff |
annotate
|
| Wed, 10 Dec 2014 19:24:54 +0100 |
wenzelm |
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
|
file |
diff |
annotate
|
| Mon, 08 Dec 2014 22:42:12 +0100 |
wenzelm |
expand ML cartouches to Input.source;
|
file |
diff |
annotate
|
| Sat, 01 Nov 2014 20:19:07 +0100 |
wenzelm |
clarified syntax -- avoid overlap with command category;
|
file |
diff |
annotate
|
| Mon, 25 Aug 2014 12:58:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 22 Aug 2014 15:39:30 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 21 Aug 2014 22:48:39 +0200 |
wenzelm |
tuned signature -- define some elementary operations earlier;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 17:56:13 +0100 |
wenzelm |
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 13:18:10 +0100 |
wenzelm |
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 16:16:28 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 11:07:47 +0100 |
wenzelm |
tuned signature -- rearranged modules;
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 22:57:50 +0100 |
wenzelm |
tuned signature -- clarified module name;
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 21:58:48 +0100 |
wenzelm |
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
|
file |
diff |
annotate
|
| Sat, 08 Mar 2014 21:08:10 +0100 |
wenzelm |
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 13:11:08 +0100 |
wenzelm |
clarified init_assignable: make double-sure that initial values are reset;
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 10:40:04 +0100 |
wenzelm |
more explicit method reports;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 11:14:38 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 10:40:13 +0100 |
wenzelm |
method language markup, e.g. relevant to prevent outer keyword completion;
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 17:25:03 +0100 |
wenzelm |
prefer user-space tool within Pure.thy;
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 17:17:26 +0100 |
wenzelm |
more markup;
|
file |
diff |
annotate
|
| Wed, 22 Jan 2014 16:03:11 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 20:35:50 +0200 |
wenzelm |
added Theory.setup convenience;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 19:53:27 +0200 |
wenzelm |
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 17:01:12 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 12 Aug 2012 22:39:28 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 12 Aug 2012 20:45:34 +0200 |
wenzelm |
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
|
file |
diff |
annotate
|
| Sat, 11 Aug 2012 22:17:46 +0200 |
wenzelm |
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 22:47:30 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 21:18:38 +0100 |
wenzelm |
added ML antiquotation @{attributes};
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 17:03:07 +0200 |
wenzelm |
proper source positions for @{lemma};
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 16:53:31 +0200 |
wenzelm |
ML antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sun, 09 Jan 2011 21:33:41 +0100 |
wenzelm |
reverted 08240feb69c7 -- breaks positions of reports;
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 21:05:50 +0100 |
wenzelm |
more robust ML antiquotations -- allow original tokens without adjacent whitespace;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 23:16:32 +0200 |
wenzelm |
refer directly to structure Keyword and Parse;
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 15:52:03 +0200 |
wenzelm |
modernized naming conventions of main Isar proof elements;
|
file |
diff |
annotate
|
| Sun, 07 Feb 2010 18:04:48 +0100 |
wenzelm |
simplified interface for ML antiquotations, struct_name is always "Isabelle";
|
file |
diff |
annotate
|
| Sun, 15 Nov 2009 19:45:05 +0100 |
wenzelm |
eliminated obsolete thm position tags;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 23:05:32 +0100 |
wenzelm |
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
|
file |
diff |
annotate
|