| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:14 +0200 |
haftmann |
emphasized general nature of parameter
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:14 +0200 |
haftmann |
moved lemmas
|
file |
diff |
annotate
|
| Thu, 24 Sep 2015 12:21:19 +0200 |
traytel |
more useful properties of the relators
|
file |
diff |
annotate
|
| Thu, 27 Aug 2015 21:19:48 +0200 |
haftmann |
standardized some occurences of ancient "split" alias
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 23:05:56 +0100 |
traytel |
BNF relators preserve reflexivity
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 13:50:11 +0100 |
Andreas Lochbihler |
add monotonicity lemmas for rel_fun
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 11:28:37 +0100 |
traytel |
more complete fp_sugars for sum and prod;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:53 +0200 |
desharna |
generate 'rec_transfer' for datatypes
|
file |
diff |
annotate
|
| Tue, 16 Sep 2014 19:23:37 +0200 |
blanchet |
register 'prod' and 'sum' as datatypes, to allow N2M through them
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 13:53:34 +0200 |
desharna |
generate 'set_transfer' for BNFs
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 13:23:39 +0200 |
desharna |
generate 'rel_transfer' for BNFs
|
file |
diff |
annotate
|
| Wed, 06 Aug 2014 16:00:11 +0200 |
traytel |
handle deep nesting in N2M
|
file |
diff |
annotate
|