| Thu, 16 Jul 2015 12:23:22 +0200 |
traytel |
{r,e,d,f}tac with proper context in BNF
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
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
|
| Wed, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:43:26 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:41:54 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:41:15 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:45:42 +0200 |
blanchet |
tuning terminology
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 11:49:47 +0200 |
blanchet |
comment
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 16:22:26 +0200 |
blanchet |
made new countable tactic work with sorts other than 'type'
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:13 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 22:47:09 +0200 |
blanchet |
intelligible errors instead of tactic failures
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
made new tactic even more robust
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
fixed tactic for n-way mutual recursion, n >= 4 (balanced conjunctions confuse the tactic)
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
improved tactic further
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
improved new countability tactic
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 09:43:00 +0200 |
blanchet |
added compatibility function
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:31:38 +0200 |
blanchet |
added countable tactic for new-style datatypes
|
file |
diff |
annotate
|