src/Pure/Isar/locale.ML
Mon, 12 Mar 2012 21:31:22 +0100 wenzelm activate_notes in parallel -- to speedup main operation of locale interpretation;
Mon, 12 Mar 2012 20:44:10 +0100 wenzelm refined activate_notes: simultaneous transformation before activation;
Sun, 11 Mar 2012 22:06:12 +0100 wenzelm tuned;
Sat, 10 Mar 2012 23:00:07 +0100 wenzelm clarified idents for activated locales, with subtle change of semantics: insert/merge wrt. term equality, but avoid redundant_ident on retrieval;
Sat, 10 Mar 2012 21:25:59 +0100 wenzelm clarified total_ident_ord, swapping first argument back to normal (unlike e464f84f3680) -- NB: "fast" ord is erratic anyway;
Sat, 10 Mar 2012 20:58:40 +0100 wenzelm misc tuning and simplification;
Sat, 10 Mar 2012 20:02:15 +0100 wenzelm tuned;
Sun, 20 Nov 2011 17:57:09 +0100 wenzelm tuned signature;
Sat, 19 Nov 2011 16:16:33 +0100 wenzelm simplified Locale.add_thmss, after partial evaluation of attributes;
Sat, 19 Nov 2011 15:04:36 +0100 wenzelm tuned;
Mon, 14 Nov 2011 20:25:22 +0100 wenzelm tuned;
Mon, 14 Nov 2011 16:52:19 +0100 wenzelm pass positions for named targets, for formal links in the document model;
Mon, 07 Nov 2011 17:00:23 +0100 wenzelm tuned signature -- avoid spurious Thm.mixed_attribute;
Fri, 28 Oct 2011 17:15:52 +0200 wenzelm tuned signature -- refined terminology;
Sun, 17 Apr 2011 19:54:04 +0200 wenzelm report Name_Space.declare/define, relatively to context;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Sat, 16 Apr 2011 13:48:45 +0200 wenzelm Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
Thu, 06 Jan 2011 21:06:18 +0100 ballarin Diagnostic command to show locale dependencies.
Sat, 18 Dec 2010 18:43:16 +0100 ballarin Add mixins to locale dependencies.
Sat, 18 Dec 2010 18:43:13 +0100 ballarin Add mixins to sublocale command.
Sun, 28 Nov 2010 15:28:48 +0100 wenzelm superficial tuning;
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
Sun, 05 Sep 2010 21:41:24 +0200 wenzelm turned show_sorts/show_types into proper configuration options;
Fri, 27 Aug 2010 12:57:55 +0200 wenzelm merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
Thu, 26 Aug 2010 16:00:54 +0200 ballarin For sublocale it is sufficient to reconsider ancestors of the target.
Thu, 26 Aug 2010 15:48:08 +0200 wenzelm renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
Thu, 26 Aug 2010 13:09:12 +0200 wenzelm renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
Tue, 10 Aug 2010 22:26:23 +0200 ballarin Revert performance improvement of 8ed3a5fb4d25 since it breaks notes element declarations.
Thu, 05 Aug 2010 22:29:43 +0200 ballarin Remove duplicate locale activation code; performance improvement.
Sat, 31 Jul 2010 23:58:05 +0200 ballarin More consistent naming of locale api functions.
Sat, 31 Jul 2010 21:14:20 +0200 ballarin print_interps shows interpretations in proofs.
Sat, 31 Jul 2010 21:14:20 +0200 ballarin Make registrations generic data.
Mon, 26 Jul 2010 14:44:07 +0200 haftmann get_registrations interface
Wed, 21 Jul 2010 09:46:36 +0200 haftmann abstract visualization of locale ingredients; all_locales yields proper locale identifiers
Tue, 22 Jun 2010 19:46:16 +0200 ballarin Proper treatment of non-inherited mixins.
Sun, 20 Jun 2010 19:02:41 +0200 haftmann separate section for diagnostic commands
Wed, 26 May 2010 21:20:18 +0200 ballarin Merge mixins of distinct interpretations with same base.
Mon, 24 May 2010 10:48:32 +0200 ballarin Store registrations in efficient data structure.
Mon, 24 May 2010 10:48:32 +0200 ballarin Avoid recomputation of registration instance for lookup.
Mon, 24 May 2010 10:48:32 +0200 ballarin Consistently use equality for registration lookup.
Mon, 24 May 2010 10:48:32 +0200 ballarin Cleaner implementation of sublocale command.
Mon, 24 May 2010 10:48:32 +0200 ballarin Reapply mixin patch: base for performance improvements.
Fri, 14 May 2010 21:23:29 +0200 ballarin Revert mixin patch due to inacceptable performance drop.
Thu, 13 May 2010 13:30:16 +0200 ballarin Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
Tue, 04 May 2010 20:30:22 +0200 ballarin Merged.
Tue, 04 May 2010 19:57:55 +0200 ballarin Provide internal function for printing a single interpretation.
Tue, 27 Apr 2010 22:27:22 +0200 ballarin Explicitly manage export in dependencies.
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;
Tue, 20 Apr 2010 22:34:17 +0200 ballarin Remove garbage.
Tue, 20 Apr 2010 22:31:08 +0200 ballarin Remove garbage.
Wed, 07 Apr 2010 19:17:10 +0200 ballarin Merged resolving conflicts NEWS and locale.ML.
Fri, 02 Apr 2010 13:33:48 +0200 ballarin Proper inheritance of mixins for activated facts and locale dependencies.
Mon, 15 Feb 2010 19:54:54 +0100 ballarin Removed obsolete function.
Mon, 15 Feb 2010 01:34:08 +0100 ballarin Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
Thu, 11 Feb 2010 21:00:36 +0100 ballarin A rough implementation of full mixin inheritance; additional unit tests.
Tue, 02 Feb 2010 21:23:20 +0100 ballarin Clarified invariant; tuned.
Mon, 01 Feb 2010 21:55:00 +0100 ballarin Use serial to be more debug friendly.
Mon, 15 Mar 2010 18:59:16 +0100 wenzelm replaced type_syntax/term_syntax by uniform syntax_declaration;
Thu, 12 Nov 2009 22:02:11 +0100 wenzelm eliminated obsolete "internal" kind -- collapsed to unspecific "";
Mon, 09 Nov 2009 21:33:22 +0100 ballarin Removed obsolete code.
less more (0) -300 -100 -60 tip