Fri, 28 Nov 2008 17:43:06 +0100 |
ballarin |
Intro_locales_tac to simplify goals involving locale predicates.
|
file |
diff |
annotate
|
Fri, 28 Nov 2008 12:26:14 +0100 |
ballarin |
Ahere to modern naming conventions; proper treatment of internal vs external names.
|
file |
diff |
annotate
|
Thu, 27 Nov 2008 21:25:34 +0100 |
ballarin |
Proper treatment of expressions with free arguments.
|
file |
diff |
annotate
|
Thu, 27 Nov 2008 10:29:07 +0100 |
ballarin |
Sublocale command.
|
file |
diff |
annotate
|
Tue, 25 Nov 2008 18:06:21 +0100 |
ballarin |
Expression types cleaned up, proper treatment of term patterns.
|
file |
diff |
annotate
|
Mon, 24 Nov 2008 18:03:48 +0100 |
ballarin |
Read/cert_statement for theorem statements.
|
file |
diff |
annotate
|
Fri, 21 Nov 2008 18:01:39 +0100 |
ballarin |
add_locale functional.
|
file |
diff |
annotate
|
Thu, 20 Nov 2008 14:55:28 +0100 |
haftmann |
tuned name bindings
|
file |
diff |
annotate
|
Thu, 20 Nov 2008 10:29:35 +0100 |
ballarin |
Deleted debug message (PolyML).
|
file |
diff |
annotate
|
Wed, 19 Nov 2008 17:04:29 +0100 |
ballarin |
Type inference for elements through syntax module.
|
file |
diff |
annotate
|
Tue, 18 Nov 2008 09:40:06 +0100 |
ballarin |
Activate elements moved to element.ML.
|
file |
diff |
annotate
|
Fri, 14 Nov 2008 16:49:52 +0100 |
ballarin |
Initial part of locale reimplementation.
|
file |
diff |
annotate
|
Tue, 28 Oct 2008 12:28:14 +0100 |
haftmann |
making SMLNJ happy
|
file |
diff |
annotate
|
Mon, 27 Oct 2008 16:23:54 +0100 |
ballarin |
New-style locale expressions with instantiation (new file expression.ML).
|
file |
diff |
annotate
|