| Mon, 03 Feb 2014 13:45:54 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 17 Dec 2013 20:21:22 +0100 |
haftmann |
initalize locale with idents from background theory rather than empty idents: must treat idents and registrations synchronously to provide consistent setup for interpretation in locale contexts
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 20:35:50 +0200 |
wenzelm |
added Theory.setup convenience;
|
file |
diff |
annotate
|
| Mon, 19 Aug 2013 20:37:36 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 14:13:18 +0200 |
wenzelm |
recovered Locale.intern from d51bac27d4a0 (still used in AFP/Simp);
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 20:58:15 +0200 |
wenzelm |
more markup -- avoid old Locale.extern;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 21:40:56 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Tue, 21 May 2013 17:45:53 +0200 |
wenzelm |
more markup;
|
file |
diff |
annotate
|
| Sun, 21 Apr 2013 10:41:18 +0200 |
haftmann |
tuned for uniformity
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 22:36:03 +0100 |
ballarin |
Improvements to the print_dependencies command.
|
file |
diff |
annotate
|
| Mon, 25 Mar 2013 19:53:44 +0100 |
ballarin |
Fix issue related to mixins in roundup.
|
file |
diff |
annotate
|
| Fri, 30 Nov 2012 22:38:06 +0100 |
wenzelm |
print formal entities with markup;
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 14:23:33 +0200 |
wenzelm |
tuned pretty_locale/print_locale, with more basic pretty_locale_deps based on that;
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 19:07:32 +0200 |
wenzelm |
added Attrib.global_notes/local_notes/generic_notes convenience;
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 15:23:43 +0200 |
wenzelm |
clarified Named_Target.target_declaration: propagate through other levels as well;
|
file |
diff |
annotate
|
| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 10:55:08 +0100 |
wenzelm |
tuned grouping -- merely indicate order of magnitude;
|
file |
diff |
annotate
|
| Wed, 14 Mar 2012 17:52:38 +0100 |
wenzelm |
source positions for locale and class expressions;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 17:04:00 +0100 |
wenzelm |
suppress vacous notes elements, with subtle change of semantics: 'interpret' no longer pulls-in unnamed facts "by fact";
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 23:33:50 +0100 |
wenzelm |
some grouping of Par_List operations, to adjust granularity;
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 21:31:22 +0100 |
wenzelm |
activate_notes in parallel -- to speedup main operation of locale interpretation;
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 20:44:10 +0100 |
wenzelm |
refined activate_notes: simultaneous transformation before activation;
|
file |
diff |
annotate
|
| Sun, 11 Mar 2012 22:06:12 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 10 Mar 2012 20:58:40 +0100 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Sat, 10 Mar 2012 20:02:15 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 17:57:09 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 16:16:33 +0100 |
wenzelm |
simplified Locale.add_thmss, after partial evaluation of attributes;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 15:04:36 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 14 Nov 2011 20:25:22 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 14 Nov 2011 16:52:19 +0100 |
wenzelm |
pass positions for named targets, for formal links in the document model;
|
file |
diff |
annotate
|
| Mon, 07 Nov 2011 17:00:23 +0100 |
wenzelm |
tuned signature -- avoid spurious Thm.mixed_attribute;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 17:15:52 +0200 |
wenzelm |
tuned signature -- refined terminology;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 06 Jan 2011 21:06:18 +0100 |
ballarin |
Diagnostic command to show locale dependencies.
|
file |
diff |
annotate
|
| Sat, 18 Dec 2010 18:43:16 +0100 |
ballarin |
Add mixins to locale dependencies.
|
file |
diff |
annotate
|
| Sat, 18 Dec 2010 18:43:13 +0100 |
ballarin |
Add mixins to sublocale command.
|
file |
diff |
annotate
|
| Sun, 28 Nov 2010 15:28:48 +0100 |
wenzelm |
superficial tuning;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 21:41:24 +0200 |
wenzelm |
turned show_sorts/show_types into proper configuration options;
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 12:57:55 +0200 |
wenzelm |
merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 16:00:54 +0200 |
ballarin |
For sublocale it is sufficient to reconsider ancestors of the target.
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 10 Aug 2010 22:26:23 +0200 |
ballarin |
Revert performance improvement of 8ed3a5fb4d25 since it breaks notes element declarations.
|
file |
diff |
annotate
|
| Thu, 05 Aug 2010 22:29:43 +0200 |
ballarin |
Remove duplicate locale activation code; performance improvement.
|
file |
diff |
annotate
|
| Sat, 31 Jul 2010 23:58:05 +0200 |
ballarin |
More consistent naming of locale api functions.
|
file |
diff |
annotate
|
| Sat, 31 Jul 2010 21:14:20 +0200 |
ballarin |
print_interps shows interpretations in proofs.
|
file |
diff |
annotate
|
| Sat, 31 Jul 2010 21:14:20 +0200 |
ballarin |
Make registrations generic data.
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 14:44:07 +0200 |
haftmann |
get_registrations interface
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 09:46:36 +0200 |
haftmann |
abstract visualization of locale ingredients; all_locales yields proper locale identifiers
|
file |
diff |
annotate
|
| Tue, 22 Jun 2010 19:46:16 +0200 |
ballarin |
Proper treatment of non-inherited mixins.
|
file |
diff |
annotate
|
| Sun, 20 Jun 2010 19:02:41 +0200 |
haftmann |
separate section for diagnostic commands
|
file |
diff |
annotate
|
| Wed, 26 May 2010 21:20:18 +0200 |
ballarin |
Merge mixins of distinct interpretations with same base.
|
file |
diff |
annotate
|
| 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
|