| 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
|