| Sun, 04 May 2014 18:14:58 +0200 |
blanchet |
renamed 'xxx_size' to 'size_xxx' for old datatype package
|
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
|
| 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:26 +0200 |
blanchet |
generate 'rec_o_map' and 'size_o_map' in size extension
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 01:02:21 +0100 |
blanchet |
balance tuples that represent curried functions
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 14:15:09 +0100 |
traytel |
rationalized imports
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 13:36:48 +0100 |
blanchet |
renamed 'map_pair' to 'map_prod'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 13:36:15 +0100 |
blanchet |
renamed 'map_sum' to 'sum_map'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 12:17:26 +0100 |
traytel |
more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms
|
file |
diff |
annotate
|
| Tue, 04 Mar 2014 18:57:17 +0100 |
blanchet |
simplify sets in BNF composition
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
make 'typedef' optional, depending on size of original type
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 17:54:52 +0100 |
traytel |
load Metis a little later
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 18:14:26 +0100 |
traytel |
joint work with blanchet: intermediate typedef for the input to fp-operations
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 22:51:11 +0100 |
blanchet |
improved accounting for dead variables when naming set functions (refines d71c2737ee21)
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 22:51:11 +0100 |
blanchet |
more precise error message
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 08:34:33 +0100 |
blanchet |
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 23:08:59 +0100 |
blanchet |
prepare two-stage 'primrec' setup
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 18:18:27 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 20:21:12 +0100 |
blanchet |
move BNF_LFP up the dependency chain
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 19:05:25 +0100 |
blanchet |
removed dependency of BNF package on Nitpick
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
made BNF compile after move to HOL
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
tuned comments
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
moved BNF files to 'HOL'
|
file |
diff |
annotate
| base
|