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