Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
use the noted theorem whenever possible, also in 'BNF_Def'
|
file |
diff |
annotate
|
Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
tuned variable names
|
file |
diff |
annotate
|
Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
repaired BNF 'size' generation tactic for datatypes mixng old- and new-style datatypes on the right-hand side
|
file |
diff |
annotate
|
Tue, 24 Jun 2014 13:48:14 +0200 |
desharna |
tune the implementation of 'rel_coinduct'
|
file |
diff |
annotate
|
Mon, 02 Jun 2014 11:59:51 +0200 |
blanchet |
removed some spurious warnings in new (co)datatype package
|
file |
diff |
annotate
|
Thu, 15 May 2014 20:48:14 +0200 |
blanchet |
more aggressive nested size handling in the absence of 'size_o_map' theorems (+ unrelated pattern matching fix)
|
file |
diff |
annotate
|
Sat, 26 Apr 2014 06:43:06 +0200 |
blanchet |
use right set of variables for recursive check
|
file |
diff |
annotate
|
Fri, 25 Apr 2014 12:09:15 +0200 |
blanchet |
more unfolding and more folding in size equations, to look more natural in the nested case
|
file |
diff |
annotate
|
Thu, 24 Apr 2014 21:00:00 +0200 |
blanchet |
really unfold
|
file |
diff |
annotate
|
Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
qualify name
|
file |
diff |
annotate
|
Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
localize new size function generation code
|
file |
diff |
annotate
|
Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
no need to make 'size' generation an interpretation -- overkill
|
file |
diff |
annotate
|
Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
pick up all 'nesting' theorems
|
file |
diff |
annotate
|
Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
prevent tactic failures by detecting and ignoring BNFs with no 'size' functions early
|
file |
diff |
annotate
|
Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
move size hooks together, with new one preceding old one and sharing same theory data
|
file |
diff |
annotate
|
Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
allow registration of custom size functions for BNF-based datatypes
|
file |
diff |
annotate
|
Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
generate 'rec_o_map' and 'size_o_map' in size extension
|
file |
diff |
annotate
|
Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
|
file |
diff |
annotate
|
Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
generate size instances for new-style datatypes
|
file |
diff |
annotate
|