| 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
|
| Sat, 22 May 2010 19:17:18 -0700 |
huffman |
HOLCF no longer redefines 'consts' command
|
changeset |
files
|
| Sat, 22 May 2010 18:34:38 -0700 |
huffman |
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
|
changeset |
files
|
| Sat, 22 May 2010 17:57:16 -0700 |
huffman |
simplify fixrec continuity tactic
|
changeset |
files
|
| Sun, 23 May 2010 22:56:45 +0200 |
krauss |
used sledgehammer[isar_proof] to replace slow metis call
|
changeset |
files
|
| Sun, 23 May 2010 17:23:18 +0100 |
webertj |
Typo fixed.
|
changeset |
files
|
| Sun, 23 May 2010 17:22:30 +0100 |
webertj |
Typo fixed.
|
changeset |
files
|