| Mon, 01 Oct 2018 16:41:36 +0200 |
wenzelm |
more direct implementation of distinct_subgoals_tac -- potentially more efficient;
|
file |
diff |
annotate
|
| Tue, 28 Aug 2018 10:58:43 +0200 |
wenzelm |
clarified signature: do not expose internal operation;
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 15:44:46 +0100 |
wenzelm |
eliminated ASCII syntax from Pure bootstrap;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 22:26:11 +0200 |
wenzelm |
eliminated atac, rtac, etac, dtac, ftac;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2015 22:20:22 +0200 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2015 22:19:36 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2015 22:16:39 +0200 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2015 11:54:20 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 20:47:29 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
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
|
| Sat, 20 Dec 2014 22:23:37 +0100 |
wenzelm |
proper context for "net" tactics;
|
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
|
| Sun, 09 Nov 2014 14:08:00 +0100 |
wenzelm |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
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
|
| Wed, 29 May 2013 18:25:11 +0200 |
wenzelm |
tuned signature -- more explicit flags for low-level Thm.bicompose;
|
file |
diff |
annotate
|
| Mon, 20 May 2013 17:14:39 +0200 |
wenzelm |
more precise treatment of theory vs. Proof.context;
|
file |
diff |
annotate
|
| Wed, 03 Apr 2013 16:45:14 +0200 |
wenzelm |
tuned -- Drule.comp_no_flatten includes Drule.incr_indexes already (NB: result should be deterministic by construction);
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 21:46:04 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 11 Nov 2012 20:31:46 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 17:47:23 +0200 |
wenzelm |
clarified defer/prefer: more specific errors;
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 15:00:19 +0100 |
wenzelm |
simplified cut_tac (cf. d549b5b0f344);
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 21:31:26 +0100 |
wenzelm |
eliminated odd/obsolete innermost_params (cf. a77ad6c86564, 3458b0e955ac);
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 17:11:33 +0100 |
wenzelm |
eliminated obsolete aliases;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:41:32 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 18:06:29 +0200 |
wenzelm |
proper context for rule_by_tactic;
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 20:30:50 +0200 |
wenzelm |
eliminanated some unreferenced identifiers;
|
file |
diff |
annotate
|