| Fri, 19 Dec 2008 11:07:36 +0100 |
ballarin |
Add inherited registrations.
|
file |
diff |
annotate
|
| Wed, 17 Dec 2008 15:21:23 +0100 |
ballarin |
Transfer theorems in print_locale.
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 20:18:46 +0100 |
ballarin |
Transfer morphism with theory closure.
|
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 14:29:05 +0100 |
ballarin |
Transfer theorems before activation.
|
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
|
| 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 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:02:57 +0100 |
haftmann |
Locale.*note* with conventional argument type
|
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 12:26:14 +0100 |
ballarin |
Ahere to modern naming conventions; proper treatment of internal vs external names.
|
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:16 +0100 |
ballarin |
Roundup bound.
|
file |
diff |
annotate
|
| Thu, 27 Nov 2008 10:28:27 +0100 |
ballarin |
Command to add dependencies, fixed processing of dependencies.
|
file |
diff |
annotate
|
| Mon, 24 Nov 2008 18:02:52 +0100 |
ballarin |
Generalised activation code.
|
file |
diff |
annotate
|
| Fri, 21 Nov 2008 18:01:39 +0100 |
ballarin |
add_locale functional.
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 19:06:05 +0100 |
haftmann |
Locale.local_note_qualified
|
file |
diff |
annotate
|
| Wed, 19 Nov 2008 17:03:13 +0100 |
ballarin |
Use 'if' in connection with 'is_some' and 'the'.
|
file |
diff |
annotate
|
| Tue, 18 Nov 2008 09:40:44 +0100 |
ballarin |
add_thmss
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 14:03:39 +0100 |
ballarin |
Generic activation of locales.
|
file |
diff |
annotate
|
| Fri, 14 Nov 2008 16:49:52 +0100 |
ballarin |
Initial part of locale reimplementation.
|
file |
diff |
annotate
|