| Fri, 16 May 2014 12:56:39 +0200 |
blanchet |
proper handling of 'ctor_dtor' for mutual corecursive cases where not all type variables are present in all low-level constructors (cf. 'coind_wit1' etc. in 'Misc_Codatatypes.thy')
|
file |
diff |
annotate
|
| Mon, 12 May 2014 17:42:54 +0200 |
desharna |
generate 'set_empty' theorem for BNFs
|
file |
diff |
annotate
|
| Mon, 28 Apr 2014 00:54:31 +0200 |
blanchet |
restored naming trick
|
file |
diff |
annotate
|
| Mon, 28 Apr 2014 00:54:30 +0200 |
blanchet |
cleaner 'rel_inject' theorems
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 11:29:39 +0200 |
blanchet |
made SML/NJ happier
|
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 |
manual merge + added 'rel_distincts' field to record for symmetry
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
reverted rb458558cbcc2 -- better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the low-level recursor) and 'rec'
|
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 |
generate size instances for new-style datatypes
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
invoke 'fp_sugar' interpretation hook on mutually recursive clique
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:17 +0200 |
kuncar |
revert idiomatic handling of namings from 5a93b8f928a2 because in combination with Named_Target.theory_init global names are sometimes created
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:16 +0200 |
kuncar |
don't forget to init Interpretation and transfer theorems in the interpretation hook
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:16 +0200 |
kuncar |
export theorems
|
file |
diff |
annotate
|