| Mon, 24 May 2010 21:18:22 +0100 |
webertj |
Typo fixed.
|
changeset |
files
|
| Mon, 24 May 2010 12:42:17 -0700 |
huffman |
move HOLCF/Sum_Cpo.thy to HOLCF/Library
|
changeset |
files
|
| Mon, 24 May 2010 12:10:24 -0700 |
huffman |
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
|
changeset |
files
|
| Mon, 24 May 2010 11:29:49 -0700 |
huffman |
move unused pattern match syntax stuff into HOLCF/ex
|
changeset |
files
|
| Mon, 24 May 2010 09:32:52 -0700 |
huffman |
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
|
changeset |
files
|
| Mon, 24 May 2010 13:48:57 +0200 |
haftmann |
more lemmas
|
changeset |
files
|
| Mon, 24 May 2010 13:48:56 +0200 |
haftmann |
induction and case rules
|
changeset |
files
|
| Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Store registrations in efficient data structure.
|
changeset |
files
|
| Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Avoid recomputation of registration instance for lookup.
|
changeset |
files
|
| Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Consistently use equality for registration lookup.
|
changeset |
files
|
| Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Cleaner implementation of sublocale command.
|
changeset |
files
|
| Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Reapply mixin patch: base for performance improvements.
|
changeset |
files
|
| Sun, 23 May 2010 19:30:29 -0700 |
huffman |
merged
|
changeset |
files
|
| Sun, 23 May 2010 19:30:14 -0700 |
huffman |
declare a few more cont2cont rules
|
changeset |
files
|