| Mon, 27 Nov 2006 13:42:48 +0100 |
haftmann |
small syntax tuning
|
changeset |
files
|
| Mon, 27 Nov 2006 13:42:47 +0100 |
haftmann |
introduced Simpdata structure
|
changeset |
files
|
| Mon, 27 Nov 2006 13:42:46 +0100 |
haftmann |
added Trueprop_conv
|
changeset |
files
|
| Mon, 27 Nov 2006 13:42:42 +0100 |
haftmann |
restructured some proofs
|
changeset |
files
|
| Mon, 27 Nov 2006 13:42:41 +0100 |
haftmann |
tuned keyword setup for SML code generator
|
changeset |
files
|
| Mon, 27 Nov 2006 13:42:39 +0100 |
haftmann |
moved order arities for fun and bool to Fun/Orderings
|
changeset |
files
|
| Mon, 27 Nov 2006 13:42:33 +0100 |
haftmann |
removed HOL structure
|
changeset |
files
|
| Mon, 27 Nov 2006 13:42:30 +0100 |
haftmann |
adjusted syntax for internal code generation
|
changeset |
files
|
| Mon, 27 Nov 2006 12:12:18 +0100 |
berghofe |
Added nominal_primrec command.
|
changeset |
files
|
| Mon, 27 Nov 2006 12:11:43 +0100 |
berghofe |
Adapted to new nominal_primrec command.
|
changeset |
files
|
| Mon, 27 Nov 2006 12:11:20 +0100 |
berghofe |
Added nominal_primrec.ML
|
changeset |
files
|
| Mon, 27 Nov 2006 12:10:51 +0100 |
berghofe |
Implemented new "nominal_primrec" command for defining
|
changeset |
files
|
| Mon, 27 Nov 2006 12:09:55 +0100 |
berghofe |
Additional information about nominal datatypes (descriptor,
|
changeset |
files
|
| Sun, 26 Nov 2006 23:43:53 +0100 |
wenzelm |
converted legacy ML scripts;
|
changeset |
files
|
| Sun, 26 Nov 2006 23:09:25 +0100 |
aspinall |
Remove add_master_files which stripped paths for retracted files. Emacs PG already supports full paths here.
|
changeset |
files
|
| Sun, 26 Nov 2006 18:07:36 +0100 |
wenzelm |
* Pure: syntax constant for foo (binder) is called foo_binder;
|
changeset |
files
|