| Mon, 07 May 2007 16:46:42 +0200 |
paulson |
First-order variant of the fully-typed translation
|
changeset |
files
|
| Mon, 07 May 2007 14:20:32 +0200 |
haftmann |
added further equality example
|
changeset |
files
|
| Mon, 07 May 2007 09:58:07 +0200 |
haftmann |
changed 'code nofunc' to 'code func del'
|
changeset |
files
|
| Mon, 07 May 2007 00:52:25 +0200 |
wenzelm |
* Context data interfaces;
|
changeset |
files
|
| Mon, 07 May 2007 00:50:09 +0200 |
wenzelm |
simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
|
changeset |
files
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
changeset |
files
|
| Sun, 06 May 2007 21:50:17 +0200 |
haftmann |
changed code generator invocation syntax
|
changeset |
files
|
| Sun, 06 May 2007 21:49:44 +0200 |
haftmann |
PreList imports RecDef
|
changeset |
files
|
| Sun, 06 May 2007 21:49:32 +0200 |
haftmann |
dropped legacy ML binding
|
changeset |
files
|
| Sun, 06 May 2007 21:49:29 +0200 |
haftmann |
added auxiliary lemmas for proof tools
|
changeset |
files
|
| Sun, 06 May 2007 21:49:27 +0200 |
haftmann |
dropped preorders, unified syntax
|
changeset |
files
|
| Sun, 06 May 2007 21:49:26 +0200 |
haftmann |
minimal import
|
changeset |
files
|