| Tue, 13 Aug 2019 15:34:46 +0200 |
wenzelm |
added SUBPROOFS / "subproofs" method combinator, for more compact proofterms;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2019 10:27:21 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 14:12:44 +0100 |
wenzelm |
clarified signature: more types;
|
file |
diff |
annotate
|
| Wed, 31 Oct 2018 15:53:32 +0100 |
wenzelm |
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
|
file |
diff |
annotate
|
| Thu, 25 Oct 2018 21:29:08 +0200 |
wenzelm |
clarified ML position: proper markup for def/ref scopes (see also 162a4c2e97bc);
|
file |
diff |
annotate
|
| Mon, 27 Aug 2018 20:43:01 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 25 Jan 2018 11:29:52 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 24 Jan 2018 20:47:36 +0100 |
wenzelm |
clarified operations;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 18:59:33 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 20 Jul 2016 11:44:11 +0200 |
wenzelm |
moved method "use" to Pure;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2016 11:53:43 +0200 |
wenzelm |
provide dynamic facts in static context, to allow use of method_facts during static closure;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2016 11:33:56 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 07 Jun 2016 19:57:41 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 07 Jun 2016 19:55:45 +0200 |
wenzelm |
clean facts more uniformly;
|
file |
diff |
annotate
|
| Tue, 07 Jun 2016 15:44:18 +0200 |
wenzelm |
expode method_facts via dynamic method context;
|
file |
diff |
annotate
|
| Thu, 12 May 2016 22:06:18 +0200 |
wenzelm |
common entity definitions within a global or local theory context;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2016 16:33:33 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2016 17:14:27 +0200 |
wenzelm |
removed redundant Position.set_range -- already done in Position.range;
|
file |
diff |
annotate
|
| Wed, 23 Dec 2015 14:40:18 +0100 |
wenzelm |
check and report source at most once, notably in body of "match" method;
|
file |
diff |
annotate
|
| Mon, 14 Dec 2015 10:14:19 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Sun, 13 Dec 2015 21:56:15 +0100 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
| Fri, 11 Dec 2015 13:44:20 +0100 |
wenzelm |
clarified modules;
|
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
|
| Tue, 08 Dec 2015 11:28:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 18 Oct 2015 21:30:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 20:20:16 +0200 |
wenzelm |
renamed method "goals" to "goal_cases" to emphasize its meaning;
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 14:44:03 +0200 |
wenzelm |
method "goals" ignores facts;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 13:08:00 +0200 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
| Tue, 30 Jun 2015 15:20:56 +0200 |
wenzelm |
renamed "default" to "standard", to make semantically clear what it is;
|
file |
diff |
annotate
|
| Mon, 29 Jun 2015 19:27:07 +0200 |
wenzelm |
clarified static phase;
|
file |
diff |
annotate
|
| Thu, 25 Jun 2015 21:45:00 +0200 |
wenzelm |
added method "goals" for proper subgoal cases;
|
file |
diff |
annotate
|
| Mon, 22 Jun 2015 19:22:48 +0200 |
wenzelm |
added method "sleep";
|
file |
diff |
annotate
|
| Mon, 22 Jun 2015 18:55:47 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 01 May 2015 14:35:13 +0200 |
wenzelm |
clarified markup range;
|
file |
diff |
annotate
|
| Fri, 01 May 2015 13:58:06 +0200 |
wenzelm |
modifier markup for all parsed tokens;
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 13:57:37 +0200 |
wenzelm |
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
|
file |
diff |
annotate
|
| Thu, 09 Apr 2015 11:28:00 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 11:52:53 +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
|
| Thu, 02 Apr 2015 20:28:30 +0200 |
wenzelm |
proper treatment of internal method name as already checked Token.src;
|
file |
diff |
annotate
|
| Thu, 02 Apr 2015 14:11:00 +0200 |
wenzelm |
clarified method_closure;
|
file |
diff |
annotate
|
| Thu, 02 Apr 2015 11:41:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 13:55:10 +0100 |
wenzelm |
clarified Token.check_src: intern at most once;
|
file |
diff |
annotate
|
| Mon, 09 Mar 2015 20:33:33 +0100 |
wenzelm |
support structural composition (THEN_ALL_NEW) for proof methods;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 14:02:48 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 12:24:56 +0100 |
wenzelm |
more abstract type Input.source;
|
file |
diff |
annotate
|
| Wed, 12 Nov 2014 10:30:59 +0100 |
wenzelm |
more careful ML source positions, for improved PIDE markup;
|
file |
diff |
annotate
|
| Tue, 11 Nov 2014 20:11:38 +0100 |
wenzelm |
more careful ML source positions, for improved PIDE markup;
|
file |
diff |
annotate
|
| Tue, 11 Nov 2014 18:16:25 +0100 |
wenzelm |
more position information, e.g. relevant for errors in generated ML source;
|
file |
diff |
annotate
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 17:04:14 +0100 |
wenzelm |
proper context for match_tac etc.;
|
file |
diff |
annotate
|
| Sat, 08 Nov 2014 21:31:51 +0100 |
wenzelm |
optional proof context for unify operations, for the sake of proper local options;
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 16:20:46 +0100 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 13:25:12 +0200 |
wenzelm |
intern xthm only once;
|
file |
diff |
annotate
|
| Wed, 27 Aug 2014 14:54:32 +0200 |
wenzelm |
more explicit Method.modifier with reported position;
|
file |
diff |
annotate
|
| Fri, 22 Aug 2014 15:55:24 +0200 |
wenzelm |
attach modifier only later, to avoid interference as e.g. in "simp add: foo [simplified] bar";
|
file |
diff |
annotate
|