| Tue, 11 Jun 2013 19:11:31 -0400 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 11 Jun 2013 18:50:09 -0400 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 11 Jun 2013 16:13:19 -0400 |
smolkas |
make use of show_type_emphasis instead of using hack; make sure global configurations don't affect proof script creation
|
changeset |
files
|
| Tue, 11 Jun 2013 21:07:53 +0200 |
haftmann |
reflexive nbe equation for equality on String.literal
|
changeset |
files
|
| Mon, 10 Jun 2013 20:43:17 +0200 |
haftmann |
tuned whitespace
|
changeset |
files
|
| Mon, 10 Jun 2013 20:30:23 +0200 |
haftmann |
dropped relics of ancient binary numeral case study
|
changeset |
files
|
| Mon, 10 Jun 2013 16:04:34 +0200 |
nipkow |
merged
|
changeset |
files
|
| Mon, 10 Jun 2013 16:04:18 +0200 |
nipkow |
all headings in upper case
|
changeset |
files
|
| Mon, 10 Jun 2013 06:08:17 -0700 |
huffman |
more int/nat transfer rules; examples of new untransferred attribute
|
changeset |
files
|
| Mon, 10 Jun 2013 06:08:14 -0700 |
huffman |
more transfer rules for sets
|
changeset |
files
|
| Mon, 10 Jun 2013 06:08:12 -0700 |
huffman |
implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
|
changeset |
files
|
| Mon, 10 Jun 2013 08:39:48 -0400 |
blanchet |
use right context when exporting variables (cf. AFP Coinductive_List failures)
|
changeset |
files
|
| Mon, 10 Jun 2013 00:30:30 -0400 |
blanchet |
keep track of nested BNFs
|
changeset |
files
|
| Mon, 10 Jun 2013 00:30:29 -0400 |
blanchet |
tuning
|
changeset |
files
|