| Tue, 30 Dec 2008 08:18:54 +0100 |
ballarin |
Temporarily avoid type errors in parse phase.
|
file |
diff |
annotate
|
| Fri, 19 Dec 2008 16:39:23 +0100 |
ballarin |
All logics ported to new locales.
|
file |
diff |
annotate
|
| Wed, 17 Dec 2008 15:20:33 +0100 |
ballarin |
Attributes not applied in foundational version of fact.
|
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
|
| Sun, 14 Dec 2008 15:43:04 +0100 |
ballarin |
Strict prefixes in locales expressions.
|
file |
diff |
annotate
|
| Fri, 12 Dec 2008 19:58:26 +0100 |
ballarin |
Propagate theorems to registrations.
|
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 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
|
| 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 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: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 11:26:07 +0100 |
ballarin |
Interpretation in theories including interaction with subclass relation.
|
file |
diff |
annotate
|
| Mon, 01 Dec 2008 16:59:31 +0100 |
ballarin |
No resolution of patterns within context statements.
|
file |
diff |
annotate
|
| Mon, 01 Dec 2008 13:43:32 +0100 |
ballarin |
Methods intro_locales and unfold_locales apply to both old and new locales.
|
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 11:14:13 +0100 |
ballarin |
Perform higher-order pattern matching during round-up.
|
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:30:42 +0100 |
ballarin |
Tests for sublocale command.
|
file |
diff |
annotate
|
| Tue, 25 Nov 2008 18:06:49 +0100 |
ballarin |
Test for term patterns added.
|
file |
diff |
annotate
|
| Mon, 24 Nov 2008 18:05:20 +0100 |
ballarin |
Some regression tests for theorem statements.
|
file |
diff |
annotate
|
| Fri, 21 Nov 2008 18:02:19 +0100 |
ballarin |
Regression tests for new locale implementation.
|
file |
diff |
annotate
|