Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Store registrations in efficient data structure.
|
file |
diff |
annotate
|
Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Avoid recomputation of registration instance for lookup.
|
file |
diff |
annotate
|
Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Consistently use equality for registration lookup.
|
file |
diff |
annotate
|
Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Cleaner implementation of sublocale command.
|
file |
diff |
annotate
|
Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Reapply mixin patch: base for performance improvements.
|
file |
diff |
annotate
|
Fri, 14 May 2010 21:23:29 +0200 |
ballarin |
Revert mixin patch due to inacceptable performance drop.
|
file |
diff |
annotate
|
Thu, 13 May 2010 13:30:16 +0200 |
ballarin |
Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
|
file |
diff |
annotate
|
Tue, 04 May 2010 20:30:22 +0200 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Tue, 04 May 2010 19:57:55 +0200 |
ballarin |
Provide internal function for printing a single interpretation.
|
file |
diff |
annotate
|
Tue, 27 Apr 2010 22:27:22 +0200 |
ballarin |
Explicitly manage export in dependencies.
|
file |
diff |
annotate
|
Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
Tue, 20 Apr 2010 22:34:17 +0200 |
ballarin |
Remove garbage.
|
file |
diff |
annotate
|
Tue, 20 Apr 2010 22:31:08 +0200 |
ballarin |
Remove garbage.
|
file |
diff |
annotate
|
Wed, 07 Apr 2010 19:17:10 +0200 |
ballarin |
Merged resolving conflicts NEWS and locale.ML.
|
file |
diff |
annotate
|
Fri, 02 Apr 2010 13:33:48 +0200 |
ballarin |
Proper inheritance of mixins for activated facts and locale dependencies.
|
file |
diff |
annotate
|
Mon, 15 Feb 2010 19:54:54 +0100 |
ballarin |
Removed obsolete function.
|
file |
diff |
annotate
|
Mon, 15 Feb 2010 01:34:08 +0100 |
ballarin |
Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
|
file |
diff |
annotate
|
Thu, 11 Feb 2010 21:00:36 +0100 |
ballarin |
A rough implementation of full mixin inheritance; additional unit tests.
|
file |
diff |
annotate
|
Tue, 02 Feb 2010 21:23:20 +0100 |
ballarin |
Clarified invariant; tuned.
|
file |
diff |
annotate
|
Mon, 01 Feb 2010 21:55:00 +0100 |
ballarin |
Use serial to be more debug friendly.
|
file |
diff |
annotate
|
Mon, 15 Mar 2010 18:59:16 +0100 |
wenzelm |
replaced type_syntax/term_syntax by uniform syntax_declaration;
|
file |
diff |
annotate
|
Thu, 12 Nov 2009 22:02:11 +0100 |
wenzelm |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
file |
diff |
annotate
|
Mon, 09 Nov 2009 21:33:22 +0100 |
ballarin |
Removed obsolete code.
|
file |
diff |
annotate
|
Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
Wed, 28 Oct 2009 16:25:27 +0100 |
wenzelm |
conceal internal bindings;
|
file |
diff |
annotate
|
Sun, 25 Oct 2009 13:04:06 +0100 |
wenzelm |
make SML/NJ happy;
|
file |
diff |
annotate
|
Sat, 24 Oct 2009 20:54:08 +0200 |
wenzelm |
maintain explicit name space kind;
|
file |
diff |
annotate
|
Sat, 24 Oct 2009 19:47:37 +0200 |
wenzelm |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file |
diff |
annotate
|
Sat, 24 Oct 2009 19:20:03 +0200 |
wenzelm |
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
|
file |
diff |
annotate
|
Thu, 15 Oct 2009 22:06:43 +0200 |
ballarin |
Observe order of declaration when printing registrations.
|
file |
diff |
annotate
|
Thu, 01 Oct 2009 20:37:33 +0200 |
ballarin |
Avoid administrative overhead for identity mixins.
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 22:15:54 +0200 |
ballarin |
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
|
file |
diff |
annotate
|
Sun, 27 Sep 2009 11:50:27 +0200 |
ballarin |
Archive registrations by external view.
|
file |
diff |
annotate
|
Sat, 19 Sep 2009 18:43:11 +0200 |
ballarin |
Explicit management of registration mixins.
|
file |
diff |
annotate
|
Wed, 19 Aug 2009 19:35:46 +0200 |
ballarin |
Improved comments and api names.
|
file |
diff |
annotate
|
Mon, 20 Jul 2009 16:49:05 +0200 |
haftmann |
dropped add_registration interface in locale
|
file |
diff |
annotate
|
Wed, 15 Jul 2009 18:20:08 +0200 |
haftmann |
simplification of locale interfaces
|
file |
diff |
annotate
|
Fri, 10 Jul 2009 07:59:29 +0200 |
haftmann |
tuned locale interface
|
file |
diff |
annotate
|
Sun, 29 Mar 2009 18:06:14 +0200 |
wenzelm |
simplified Element.activate(_i): singleton version;
|
file |
diff |
annotate
|
Sun, 29 Mar 2009 17:47:50 +0200 |
wenzelm |
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
|
file |
diff |
annotate
|
Sun, 29 Mar 2009 16:13:24 +0200 |
wenzelm |
simplified roundup activation interface;
|
file |
diff |
annotate
|
Sat, 28 Mar 2009 20:25:23 +0100 |
wenzelm |
simplified Locale.activate operations, using generic context;
|
file |
diff |
annotate
|
Sat, 28 Mar 2009 17:53:33 +0100 |
wenzelm |
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
|
file |
diff |
annotate
|
Sat, 28 Mar 2009 17:21:11 +0100 |
wenzelm |
renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
|
file |
diff |
annotate
|
Sat, 28 Mar 2009 16:00:54 +0100 |
wenzelm |
simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
|
file |
diff |
annotate
|
Sat, 28 Mar 2009 12:48:31 +0100 |
wenzelm |
minor tuning;
|
file |
diff |
annotate
|
Thu, 26 Mar 2009 17:00:59 +0100 |
wenzelm |
register_locale: produce stamps at the spot where elements are registered;
|
file |
diff |
annotate
|
Thu, 19 Mar 2009 13:28:55 +0100 |
wenzelm |
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
|
file |
diff |
annotate
|
Fri, 13 Mar 2009 23:50:05 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
Thu, 12 Mar 2009 11:10:02 +0100 |
wenzelm |
renamed NameSpace.bind to NameSpace.define;
|
file |
diff |
annotate
|
Wed, 11 Mar 2009 16:36:27 +0100 |
wenzelm |
eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
|
file |
diff |
annotate
|
Sat, 07 Mar 2009 22:16:50 +0100 |
wenzelm |
more uniform handling of binding in targets and derived elements;
|
file |
diff |
annotate
|
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
|