| 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
|