| Tue, 16 May 2023 17:08:31 +0200 |
wenzelm |
clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
|
file |
diff |
annotate
|
| Mon, 15 May 2023 22:46:04 +0200 |
wenzelm |
proper transfer to supported "bundle ... begin unbundle ... end", e.g. see theory "AFP/Probabilistic_Timed_Automata.Graphs";
|
file |
diff |
annotate
|
| Sat, 22 Apr 2023 21:00:24 +0200 |
wenzelm |
tuned: concise combinators instead of bulky case-expressions;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2021 21:16:22 +0200 |
wenzelm |
export other entities, e.g. relevant for formal document output;
|
file |
diff |
annotate
|
| Thu, 05 Aug 2021 07:12:49 +0000 |
haftmann |
antiquotation for bundles
|
file |
diff |
annotate
|
| Sun, 15 Nov 2020 07:17:05 +0000 |
haftmann |
type alias for mixin bundles
|
file |
diff |
annotate
|
| Thu, 29 Oct 2020 18:23:28 +0000 |
haftmann |
unified Local_Theory.init with Generic_Target.init
|
file |
diff |
annotate
|
| Sat, 24 Oct 2020 14:40:12 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 12 Oct 2020 07:25:38 +0000 |
haftmann |
dedicated module for toplevel target handling
|
file |
diff |
annotate
|
| Mon, 12 Oct 2020 07:25:38 +0000 |
haftmann |
avoid _cmd suffix where no Isar command is involved
|
file |
diff |
annotate
|
| Mon, 12 Oct 2020 07:25:38 +0000 |
haftmann |
consolidated names and operations
|
file |
diff |
annotate
|
| Mon, 12 Oct 2020 07:25:38 +0000 |
haftmann |
centralized case distinction for beginning and ending nested targets in one place
|
file |
diff |
annotate
|
| Sat, 10 Oct 2020 18:51:40 +0000 |
haftmann |
direct exit to theory when ending nested target on theory target
|
file |
diff |
annotate
|
| Sat, 10 Oct 2020 18:43:10 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sat, 10 Oct 2020 18:43:07 +0000 |
haftmann |
avoid baroque export
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 19:18:49 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 16 Feb 2018 18:28:44 +0100 |
wenzelm |
trim context of persistent data;
|
file |
diff |
annotate
|
| Fri, 04 Aug 2017 08:12:58 +0200 |
haftmann |
more structural sharing between common target Generic_Target.init
|
file |
diff |
annotate
|
| Fri, 04 Aug 2017 08:12:57 +0200 |
haftmann |
exit always refers to the bottom of a nested local theory stack, after_close always to all non-bottom elements
|
file |
diff |
annotate
|
| Fri, 04 Aug 2017 08:12:54 +0200 |
haftmann |
treat exit separate from regular local theory operations
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 10 Jun 2016 22:47:25 +0200 |
wenzelm |
added command 'unbundle';
|
file |
diff |
annotate
|
| Fri, 10 Jun 2016 16:28:48 +0200 |
wenzelm |
avoid duplicate Attrib.local_notes in aux. context;
|
file |
diff |
annotate
|
| Fri, 10 Jun 2016 16:17:33 +0200 |
wenzelm |
proper restore;
|
file |
diff |
annotate
|
| Fri, 10 Jun 2016 13:48:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2016 15:41:49 +0200 |
wenzelm |
support for bundle definition via target;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2016 12:02:38 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 20 Apr 2016 11:33:45 +0200 |
wenzelm |
invisible context similar to interpretation;
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 16:10:13 +0100 |
wenzelm |
prefer non-ASCII output;
|
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
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Sun, 14 Jun 2015 15:53:13 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 20:03:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2015 19:56:51 +0200 |
wenzelm |
more uniform "verbose" option to print name space;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 13:32:32 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 17:34:52 +0200 |
wenzelm |
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:35:39 +0200 |
wenzelm |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
file |
diff |
annotate
|
| Tue, 11 Mar 2014 14:28:39 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 15:04:01 +0100 |
wenzelm |
tuned signature -- prefer Name_Space.get with its builtin error;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:55:03 +0100 |
wenzelm |
abstract type Name_Space.table;
|
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, 26 Feb 2014 10:53:19 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 20 Aug 2013 20:29:38 +0200 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2013 17:38:54 +0100 |
wenzelm |
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
|
file |
diff |
annotate
|
| Fri, 30 Nov 2012 22:38:06 +0100 |
wenzelm |
print formal entities with markup;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 20:08:08 +0200 |
wenzelm |
less intrusive visibility;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 18:22:14 +0200 |
wenzelm |
close context elements via Expression.cert/read_declaration;
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 21:46:45 +0200 |
wenzelm |
more general context command with auxiliary fixes/assumes etc.;
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 20:42:19 +0200 |
wenzelm |
nothing specific about named target;
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 19:07:32 +0200 |
wenzelm |
added Attrib.global_notes/local_notes/generic_notes convenience;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 23:41:58 +0100 |
wenzelm |
actually expose target context;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 23:26:35 +0100 |
wenzelm |
more explicit Toplevel.open_target/close_target;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 21:24:13 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 21:06:31 +0100 |
wenzelm |
optional 'includes' element for long theorem statements;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 17:25:35 +0100 |
wenzelm |
basic support for nested contexts including bundles;
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 20:00:13 +0100 |
wenzelm |
basic support for bundled declarations;
|
file |
diff |
annotate
|