| Sun, 14 Jun 2015 23:22:08 +0200 |
wenzelm |
improved treatment of Element.Obtains via Expression.prepare_stmt;
|
file |
diff |
annotate
|
| Sun, 14 Jun 2015 15:53:13 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 16:35:27 +0200 |
wenzelm |
eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
|
file |
diff |
annotate
|
| Thu, 11 Jun 2015 22:47:53 +0200 |
wenzelm |
support for 'consider' command;
|
file |
diff |
annotate
|
| Thu, 11 Jun 2015 15:44:00 +0200 |
wenzelm |
support to parse obtain clause without type-checking yet;
|
file |
diff |
annotate
|
| Thu, 11 Jun 2015 11:09:05 +0200 |
wenzelm |
tuned -- eliminated unused feature;
|
file |
diff |
annotate
|
| Thu, 11 Jun 2015 10:44:04 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 16:42:17 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 20:03:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 15:01:07 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| Sun, 29 Mar 2015 21:30:28 +0200 |
wenzelm |
support for minimal specifications, with usual treatment of fixes and dummies;
|
file |
diff |
annotate
|
| Wed, 12 Nov 2014 18:18:38 +0100 |
wenzelm |
prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 17:08:54 +0100 |
wenzelm |
eliminated odd flags and hook;
|
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
|
| Fri, 09 May 2014 22:04:50 +0200 |
wenzelm |
more position markup to help locating the query context, e.g. from "Info" dockable;
|
file |
diff |
annotate
|
| Wed, 07 May 2014 13:55:16 +0200 |
wenzelm |
print results as "state", to avoid intrusion into the source text;
|
file |
diff |
annotate
|
| Mon, 17 Mar 2014 10:11:23 +0100 |
wenzelm |
reject internal names, notably from Term.free_dummy_patterns;
|
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
|
| Sun, 09 Mar 2014 16:37:56 +0100 |
wenzelm |
tuned signature;
|
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
|
| Thu, 06 Mar 2014 14:38:54 +0100 |
wenzelm |
eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 13:44:01 +0100 |
wenzelm |
more uniform check_const/read_const;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 12:43:29 +0100 |
wenzelm |
more rigid type_name demands, based on educated guesses about the tools involved here;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 12:10:19 +0100 |
wenzelm |
tuned signature -- more uniform check_type_name/read_type_name;
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 23:16:33 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Wed, 22 Jan 2014 22:32:28 +0100 |
wenzelm |
observe local syntax mode (according to e3a39dae2004, which was lost in 0f3ad56548bc), e.g. relevant for "abbreviation (output)" with non-terminating syntax;
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 16:38:17 +0100 |
wenzelm |
discontinued obsolete 'axioms' command;
|
file |
diff |
annotate
|