| Wed, 03 Sep 2014 22:49:05 +0200 |
blanchet |
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:48 +0200 |
blanchet |
tuned ctr_sugar database handling
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:35 +0200 |
blanchet |
tuned BNF database handling
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:09 +0200 |
blanchet |
intelligible errors instead of tactic failures
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
reenabled yet another example
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
made new tactic even more robust
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
reenabled more examples
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
fixed tactic for n-way mutual recursion, n >= 4 (balanced conjunctions confuse the tactic)
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
reintroduced more examples
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
improved tactic further
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
reenabled example
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
improved new countability tactic
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
more robust exception handling
|
changeset |
files
|
| Wed, 03 Sep 2014 22:46:54 +0200 |
blanchet |
added tests for new 'countable_datatype' proof method
|
changeset |
files
|
| Wed, 03 Sep 2014 12:30:25 +0200 |
traytel |
lessen the burden on the caller: sort where necessary in n2m
|
changeset |
files
|
| Wed, 03 Sep 2014 09:43:00 +0200 |
blanchet |
added compatibility function
|
changeset |
files
|
| Wed, 03 Sep 2014 00:31:38 +0200 |
blanchet |
added countable tactic for new-style datatypes
|
changeset |
files
|
| Wed, 03 Sep 2014 00:31:37 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:32 +0200 |
blanchet |
registered 'typerep' as countable again
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:30 +0200 |
blanchet |
moved old datatype material around
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:28 +0200 |
blanchet |
removed vacuous theorem references
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:27 +0200 |
blanchet |
commented out failing tactic (now that 'typerep' is defined using the new package
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:26 +0200 |
blanchet |
tuned imports
|
changeset |
files
|