| Thu, 22 Feb 2018 14:28:05 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 21 Dec 2016 17:37:58 +0100 |
blanchet |
moved and exported tactic
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:41:14 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Mon, 15 Feb 2016 12:48:10 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sun, 13 Dec 2015 21:56:15 +0100 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 13:07:40 +0100 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 17:24:54 +0200 |
wenzelm |
updated to infer_instantiate;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:47:08 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2015 17:25:44 +0200 |
blanchet |
made tactic more robust w.r.t. equations containing 'case_prod'
|
file |
diff |
annotate
|
| Thu, 16 Jul 2015 12:23:22 +0200 |
traytel |
{r,e,d,f}tac with proper context in BNF
|
file |
diff |
annotate
|
| Sun, 03 May 2015 18:14:11 +0200 |
blanchet |
made split-rule tactic go beyond constructors with 20 arguments
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 15:44:37 +0100 |
blanchet |
strengthened tactic
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 14:58:35 +0100 |
blanchet |
strengthened tactic
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2015 19:08:04 +0100 |
traytel |
eliminated some clones of Proof_Context.cterm_of
|
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
|
| Fri, 19 Dec 2014 11:20:07 +0100 |
desharna |
use proper context in function
|
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
|
| Mon, 18 Aug 2014 17:19:58 +0200 |
blanchet |
reordered some (co)datatype property names for more consistency
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 17:42:24 +0200 |
blanchet |
made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 22:30:58 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
| Thu, 06 Feb 2014 00:03:12 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 05 Feb 2014 23:30:02 +0100 |
blanchet |
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
tuned names
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
adjusted comments
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
avoid nested 'Tools' directories
|
file |
diff |
annotate
| base
|