| 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
|
| Thu, 03 Apr 2014 10:51:24 +0200 |
blanchet |
added same idiomatic handling of namings for Ctr_Sugar/BNF-related interpretation hooks as for typedef and (old-style) datatypes
|
file |
diff |
annotate
|
| Tue, 01 Apr 2014 10:51:29 +0200 |
blanchet |
added new-style (co)datatype interpretation hook
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 18:19:57 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Tue, 11 Mar 2014 17:18:42 +0100 |
blanchet |
added missing theorems to unfolding set
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 14:21:15 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 01:02:21 +0100 |
blanchet |
balance tuples that represent curried functions
|
file |
diff |
annotate
|
| Tue, 04 Mar 2014 18:57:17 +0100 |
blanchet |
register relator equations as spec rules only for datatypes -- for codatatypes they underspecify the function and are therefore dangerous (e.g. to Nitpick)
|
file |
diff |
annotate
|
| Tue, 04 Mar 2014 18:57:17 +0100 |
blanchet |
renamed a pair of low-level theorems to have c/dtor in their names (like the others)
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
removed (co)iterators from documentation
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalize internals
|
file |
diff |
annotate
|