| Sun, 06 Aug 2017 15:02:54 +0200 |
haftmann |
do not fall back on nbe if plain evaluation fails
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:28:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 17:47:28 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
file |
diff |
annotate
|
| Fri, 09 May 2014 08:13:37 +0200 |
haftmann |
hardcoded nbe and sml into value command
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 09:36:12 +0100 |
haftmann |
removed experimental equality checking of closures; acknowledge underapproximation of equality in function name
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 23:13:58 +0100 |
haftmann |
nbe decides equality of abstractions by extensionality
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 13:44:10 +0200 |
haftmann |
more explicit theory name
|
file |
diff |
annotate
| base
|