| Tue, 03 Mar 2009 18:32:01 +0100 |
wenzelm |
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:03 +0100 |
haftmann |
wrecked old locale package and related modules
|
file |
diff |
annotate
|
| Sat, 17 Jan 2009 22:07:15 +0100 |
haftmann |
exported depedencies; tuned signature
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 08:04:39 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 11 Jan 2009 14:18:17 +0100 |
haftmann |
explicit bookkeeping of intro rules and axiom
|
file |
diff |
annotate
|
| Wed, 07 Jan 2009 22:31:36 +0100 |
haftmann |
tuned signature; internal code reorganisation
|
file |
diff |
annotate
|
| Tue, 06 Jan 2009 08:50:12 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 05 Jan 2009 15:55:51 +0100 |
haftmann |
locale -> old_locale, new_locale -> locale
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 18:53:19 +0100 |
wenzelm |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 15:30:10 +0100 |
wenzelm |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 18:42:37 +0100 |
haftmann |
removed Table.extend, NameSpace.extend_table
|
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:26:46 +0100 |
ballarin |
Made global_note_qualified public.
|
file |
diff |
annotate
|
| Mon, 01 Dec 2008 19:41:16 +0100 |
haftmann |
new Binding module
|
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
|
| Thu, 27 Nov 2008 10:26:00 +0100 |
ballarin |
Fixed strange indentation.
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 19:06:05 +0100 |
haftmann |
Locale.local_note_qualified
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 14:55:28 +0100 |
haftmann |
tuned name bindings
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 17:00:27 +0100 |
haftmann |
explicit name morphism function for locale interpretation
|
file |
diff |
annotate
|
| Fri, 14 Nov 2008 14:00:52 +0100 |
ballarin |
Made local_note_prefix public.
|
file |
diff |
annotate
|
| Fri, 14 Nov 2008 08:50:10 +0100 |
haftmann |
namify and name_decl combinators
|
file |
diff |
annotate
|
| Thu, 13 Nov 2008 14:19:10 +0100 |
haftmann |
proper name morphisms for locales
|
file |
diff |
annotate
|
| Mon, 10 Nov 2008 19:42:22 +0100 |
haftmann |
restruced naming code in anticipation of introduction of name morphisms
|
file |
diff |
annotate
|
| Mon, 10 Nov 2008 08:18:58 +0100 |
haftmann |
using explicit interpretaton prefix in Name.binding (still on the surface)
|
file |
diff |
annotate
|
| Thu, 30 Oct 2008 10:57:45 +0100 |
ballarin |
Dropped context element 'includes'.
|
file |
diff |
annotate
|
| Mon, 27 Oct 2008 16:14:51 +0100 |
ballarin |
Extension of interface: declarations_of.
|
file |
diff |
annotate
|
| Fri, 26 Sep 2008 19:07:56 +0200 |
wenzelm |
eliminated polymorphic equality;
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 15:21:30 +0200 |
ballarin |
Public interface to interpretation morphism.
|
file |
diff |
annotate
|