| Thu, 07 Apr 2016 17:56:22 +0200 |
traytel |
derive (co)rec uniformly from (un)fold
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 09:54:17 +0200 |
traytel |
single uniqueness theorems for map, (un)fold, (co)rec for mutual (co)datatypes
|
file |
diff |
annotate
|
| Sun, 03 Apr 2016 10:25:17 +0200 |
traytel |
tuned names
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
generalized ML function
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
added '_legacy' suffixes
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
generalized ML interface
|
file |
diff |
annotate
|
| Tue, 22 Mar 2016 07:57:01 +0100 |
blanchet |
added timers to N2M
|
file |
diff |
annotate
|
| Tue, 22 Mar 2016 07:18:36 +0100 |
traytel |
document that n2m does not depend on most things in fp_sugar in its type
|
file |
diff |
annotate
|
| Mon, 14 Mar 2016 21:37:49 +0100 |
blanchet |
generalized ML function
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 17:08:36 +0100 |
blanchet |
making 'pred_inject' a first-class BNF citizen
|
file |
diff |
annotate
|
| Mon, 11 Jan 2016 13:15:14 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 11 Jan 2016 13:15:14 +0100 |
blanchet |
exported ML function
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 15:53:39 +0100 |
wenzelm |
more uniform treatment of package internals;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2015 17:25:48 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 19:17:41 +0200 |
blanchet |
simplified code
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:21:07 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 30 Mar 2015 22:34:59 +0200 |
wenzelm |
support for strictly private name space entries;
|
file |
diff |
annotate
|
| Mon, 30 Mar 2015 20:59:14 +0200 |
blanchet |
export more low-level theorems in data structure (partly for 'corec')
|
file |
diff |
annotate
|
| Thu, 26 Mar 2015 17:10:24 +0100 |
blanchet |
store low-level (un)fold constants
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 20:53:16 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:56:43 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2015 19:08:04 +0100 |
traytel |
eliminated some clones of Proof_Context.cterm_of
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Wed, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:41:37 +0200 |
desharna |
rename 'xtor_rel_thms' to 'xtor_rels'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:40:56 +0200 |
desharna |
rename 'xtor_set_thmss' to 'xtor_setss'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:40:31 +0200 |
desharna |
rename 'xtor_map_thms' to 'xtor_maps'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:39:12 +0200 |
desharna |
rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:38:40 +0200 |
desharna |
rename 'dtor_set_induct_thms' to 'dtor_set_inducts'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:38:13 +0200 |
desharna |
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:37:38 +0200 |
desharna |
rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:56 +0200 |
desharna |
generate 'corec_transfer' for codatatypes
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:53 +0200 |
desharna |
generate 'rec_transfer' for datatypes
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:51 +0200 |
desharna |
generate 'dtor_corec_transfer' for codatatypes
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:50 +0200 |
desharna |
generate 'ctor_rec_transfer' for datatypes
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 14:14:47 +0200 |
traytel |
goal generation for xtor_co_rec_transfer
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 09:01:14 +0200 |
traytel |
even more deads go to the end (continuation of e3a01b73579f)
|
file |
diff |
annotate
|
| Sat, 13 Sep 2014 18:08:38 +0200 |
blanchet |
imported patch phantoms
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
nicer case names in the N2M case, similar to those generated by the old package (e.g. 'Cons_tree' instead of just 'Cons')
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
moved code around
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:31:37 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
more compatibility between old- and new-style datatypes
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
made transfer functions slightly more general
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 17:19:58 +0200 |
blanchet |
reordered some (co)datatype property names for more consistency
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 10:50:28 +0200 |
desharna |
generate 'set_induct' theorem for codatatypes
|
file |
diff |
annotate
|
| Fri, 25 Jul 2014 11:26:10 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 16 Jul 2014 10:13:00 +0200 |
desharna |
generate 'rel_sel' theorem for (co)datatypes
|
file |
diff |
annotate
|
| Mon, 07 Jul 2014 16:06:46 +0200 |
desharna |
refactor some tactics
|
file |
diff |
annotate
|
| Mon, 07 Jul 2014 16:06:46 +0200 |
desharna |
generate 'rel_cases' theorem for (co)datatypes
|
file |
diff |
annotate
|
| Thu, 03 Jul 2014 11:30:02 +0200 |
desharna |
generate 'rel_intros' theorem for (co)datatypes
|
file |
diff |
annotate
|
| Wed, 02 Jul 2014 17:01:49 +0200 |
desharna |
generate 'corec_code' theorem for codatatypes
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
tuned variable names
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
no need to make 'size' generation an interpretation -- overkill
|
file |
diff |
annotate
|