Fri, 19 Dec 2008 15:05:37 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Thu, 18 Dec 2008 11:16:48 +0100 |
Norbert Schirmer |
adapted statespace module to new locales;
|
file |
diff |
annotate
|
Fri, 19 Dec 2008 14:31:07 +0100 |
ballarin |
Intro_locales_tac knows about defines elements; more robust export morphism.
|
file |
diff |
annotate
|
Thu, 18 Dec 2008 20:19:49 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Wed, 17 Dec 2008 17:53:41 +0100 |
ballarin |
Prevent defines from being checked in interpretation.
|
file |
diff |
annotate
|
Thu, 18 Dec 2008 19:52:11 +0100 |
ballarin |
Refactored: evaluate specification text only in locale declarations.
|
file |
diff |
annotate
|
Tue, 16 Dec 2008 15:08:08 +0100 |
ballarin |
Finer-grained activation so that facts from earlier elements are available.
|
file |
diff |
annotate
|
Tue, 16 Dec 2008 12:08:10 +0100 |
ballarin |
Use correct mode when parsing elements and conclusion.
|
file |
diff |
annotate
|
Sun, 14 Dec 2008 15:43:04 +0100 |
ballarin |
Strict prefixes in locales expressions.
|
file |
diff |
annotate
|
Fri, 12 Dec 2008 12:31:00 +0100 |
ballarin |
Equations in interpretation as goals.
|
file |
diff |
annotate
|
Thu, 11 Dec 2008 17:56:34 +0100 |
ballarin |
Interpretation in theories: first version with equations.
|
file |
diff |
annotate
|
Wed, 10 Dec 2008 17:19:25 +0100 |
ballarin |
Use prefix component of bindings for locale prefixes.
|
file |
diff |
annotate
|
Wed, 10 Dec 2008 16:30:33 +0100 |
ballarin |
Preserve idents (expression in sublocale).
|
file |
diff |
annotate
|
Wed, 10 Dec 2008 14:21:42 +0100 |
ballarin |
Satisfy a_axioms.
|
file |
diff |
annotate
|
Wed, 10 Dec 2008 10:12:44 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Wed, 10 Dec 2008 10:11:18 +0100 |
ballarin |
Enable keyword 'structure' in for clause of locale expression.
|
file |
diff |
annotate
|
Tue, 09 Dec 2008 22:00:39 +0100 |
ballarin |
Correct order of defines in specification.
|
file |
diff |
annotate
|
Tue, 09 Dec 2008 21:27:00 +0100 |
ballarin |
Pass on defines in inheritance; reject illicit defines created by instantiation.
|
file |
diff |
annotate
|
Tue, 09 Dec 2008 15:34:49 +0100 |
ballarin |
Order of implicit parameters in locale expression.
|
file |
diff |
annotate
|
Tue, 09 Dec 2008 11:30:24 +0100 |
ballarin |
When adding locales, delay notes until local theory is built.
|
file |
diff |
annotate
|
Mon, 08 Dec 2008 21:33:50 +0100 |
ballarin |
Default names for definitions.
|
file |
diff |
annotate
|
Mon, 08 Dec 2008 18:44:24 +0100 |
ballarin |
Proper shape of assumptions generated from Defines elements.
|
file |
diff |
annotate
|
Mon, 08 Dec 2008 14:22:42 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Mon, 08 Dec 2008 14:18:29 +0100 |
ballarin |
Explicitly close up defines.
|
file |
diff |
annotate
|
Fri, 05 Dec 2008 16:41:36 +0100 |
ballarin |
Interpretation in proof contexts.
|
file |
diff |
annotate
|
Fri, 05 Dec 2008 18:43:42 +0100 |
haftmann |
Name.name_of -> Binding.base_name
|
file |
diff |
annotate
|
Fri, 05 Dec 2008 11:42:27 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Fri, 05 Dec 2008 11:26:07 +0100 |
ballarin |
Interpretation in theories including interaction with subclass relation.
|
file |
diff |
annotate
|
Fri, 05 Dec 2008 08:04:53 +0100 |
haftmann |
dropped NameSpace.declare_base
|
file |
diff |
annotate
|
Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
Wed, 03 Dec 2008 15:27:41 +0100 |
ballarin |
Sublocale: removed public after_qed; identifiers private to NewLocale.
|
file |
diff |
annotate
|
Mon, 01 Dec 2008 16:59:31 +0100 |
ballarin |
No resolution of patterns within context statements.
|
file |
diff |
annotate
|
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
|