| 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
|
| Sat, 08 Jun 2013 19:40:19 -0700 |
huffman |
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
|
changeset |
files
|
| Fri, 07 Jun 2013 22:17:22 -0400 |
blanchet |
SPASS has more Uppercase keywords than I was fearing -- better always append _
|
changeset |
files
|
| Fri, 07 Jun 2013 22:17:19 -0400 |
blanchet |
merge
|
changeset |
files
|
| Fri, 07 Jun 2013 17:24:29 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 07 Jun 2013 17:09:07 +0100 |
blanchet |
adapted example (cf. 78a3d5006cf1)
|
changeset |
files
|
| Fri, 07 Jun 2013 17:04:55 +0100 |
blanchet |
code simplifications (cf. 78a3d5006cf1)
|
changeset |
files
|
| Fri, 07 Jun 2013 16:19:52 +0100 |
blanchet |
killed dead code
|
changeset |
files
|
| Fri, 07 Jun 2013 14:45:07 +0200 |
blanchet |
changed back type of corecursor for nested case, effectively reverting aa66ea552357 and 78a3d5006cf1
|
changeset |
files
|
| Fri, 07 Jun 2013 12:54:40 +0200 |
blanchet |
killed dead code
|
changeset |
files
|
| Fri, 07 Jun 2013 12:34:40 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 07 Jun 2013 12:11:55 +0200 |
blanchet |
tuning
|
changeset |
files
|