| Wed, 10 Dec 2008 14:21:42 +0100 |
Satisfy a_axioms.
|
file | diff | annotate |
| Wed, 10 Dec 2008 10:12:44 +0100 |
Merged.
|
file | diff | annotate |
| Wed, 10 Dec 2008 10:11:18 +0100 |
Enable keyword 'structure' in for clause of locale expression.
|
file | diff | annotate |
| Tue, 09 Dec 2008 22:00:39 +0100 |
Correct order of defines in specification.
|
file | diff | annotate |
| Tue, 09 Dec 2008 21:27:00 +0100 |
Pass on defines in inheritance; reject illicit defines created by instantiation.
|
file | diff | annotate |
| Tue, 09 Dec 2008 15:34:49 +0100 |
Order of implicit parameters in locale expression.
|
file | diff | annotate |
| Tue, 09 Dec 2008 11:30:24 +0100 |
When adding locales, delay notes until local theory is built.
|
file | diff | annotate |
| Mon, 08 Dec 2008 21:33:50 +0100 |
Default names for definitions.
|
file | diff | annotate |
| Mon, 08 Dec 2008 18:44:24 +0100 |
Proper shape of assumptions generated from Defines elements.
|
file | diff | annotate |
| Mon, 08 Dec 2008 14:22:42 +0100 |
Merged.
|
file | diff | annotate |
| Mon, 08 Dec 2008 14:18:29 +0100 |
Explicitly close up defines.
|
file | diff | annotate |
| Fri, 05 Dec 2008 16:41:36 +0100 |
Interpretation in proof contexts.
|
file | diff | annotate |
| Fri, 05 Dec 2008 18:43:42 +0100 |
Name.name_of -> Binding.base_name
|
file | diff | annotate |
| Fri, 05 Dec 2008 11:42:27 +0100 |
Merged.
|
file | diff | annotate |
| Fri, 05 Dec 2008 11:26:07 +0100 |
Interpretation in theories including interaction with subclass relation.
|
file | diff | annotate |
| Fri, 05 Dec 2008 08:04:53 +0100 |
dropped NameSpace.declare_base
|
file | diff | annotate |
| Thu, 04 Dec 2008 14:43:33 +0100 |
cleaned up binding module and related code
|
file | diff | annotate |
| Wed, 03 Dec 2008 15:27:41 +0100 |
Sublocale: removed public after_qed; identifiers private to NewLocale.
|
file | diff | annotate |
| Mon, 01 Dec 2008 16:59:31 +0100 |
No resolution of patterns within context statements.
|
file | diff | annotate |
| Fri, 28 Nov 2008 17:43:06 +0100 |
Intro_locales_tac to simplify goals involving locale predicates.
|
file | diff | annotate |
| Fri, 28 Nov 2008 12:26:14 +0100 |
Ahere to modern naming conventions; proper treatment of internal vs external names.
|
file | diff | annotate |
| Thu, 27 Nov 2008 21:25:34 +0100 |
Proper treatment of expressions with free arguments.
|
file | diff | annotate |
| Thu, 27 Nov 2008 10:29:07 +0100 |
Sublocale command.
|
file | diff | annotate |
| Tue, 25 Nov 2008 18:06:21 +0100 |
Expression types cleaned up, proper treatment of term patterns.
|
file | diff | annotate |
| Mon, 24 Nov 2008 18:03:48 +0100 |
Read/cert_statement for theorem statements.
|
file | diff | annotate |
| Fri, 21 Nov 2008 18:01:39 +0100 |
add_locale functional.
|
file | diff | annotate |
| Thu, 20 Nov 2008 14:55:28 +0100 |
tuned name bindings
|
file | diff | annotate |
| Thu, 20 Nov 2008 10:29:35 +0100 |
Deleted debug message (PolyML).
|
file | diff | annotate |
| Wed, 19 Nov 2008 17:04:29 +0100 |
Type inference for elements through syntax module.
|
file | diff | annotate |
| Tue, 18 Nov 2008 09:40:06 +0100 |
Activate elements moved to element.ML.
|
file | diff | annotate |
| Fri, 14 Nov 2008 16:49:52 +0100 |
Initial part of locale reimplementation.
|
file | diff | annotate |
| Tue, 28 Oct 2008 12:28:14 +0100 |
making SMLNJ happy
|
file | diff | annotate |
| Mon, 27 Oct 2008 16:23:54 +0100 |
New-style locale expressions with instantiation (new file expression.ML).
|
file | diff | annotate |