| Thu, 14 Aug 2014 12:13:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 13 Aug 2014 16:06:32 +0200 |
wenzelm |
tuned signature -- proper Local_Theory.add_thms_dynamic;
|
file |
diff |
annotate
|
| Wed, 13 Aug 2014 13:30:28 +0200 |
wenzelm |
load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;
|
file |
diff |
annotate
|
| Wed, 13 Aug 2014 12:59:27 +0200 |
wenzelm |
clarified terminology: first is top (amending d110b0d1bc12);
|
file |
diff |
annotate
|
| Wed, 13 Aug 2014 12:52:26 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 08 Jun 2014 23:30:52 +0200 |
haftmann |
tuned terminology: emphasize stack-like nature of nested local theories
|
file |
diff |
annotate
|
| Thu, 01 May 2014 09:30:34 +0200 |
haftmann |
prevent subscription in nested contexts explicitly -- at foundational and user level
|
file |
diff |
annotate
|
| Fri, 25 Apr 2014 21:45:04 +0200 |
haftmann |
subscription as target-specific implementation device
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 12:23:59 +0100 |
wenzelm |
back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 10:08:36 +0100 |
wenzelm |
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 10:42:28 +0100 |
wenzelm |
more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges;
|
file |
diff |
annotate
|
| Tue, 11 Mar 2014 21:58:41 +0100 |
wenzelm |
slightly more rubust (and opportunistic) exit for old-fashioned theory_to_proof, which is used by global 'sublocale' with Named_Target.init but without proper exit;
|
file |
diff |
annotate
|
| Fri, 13 Dec 2013 20:20:15 +0100 |
wenzelm |
maintain morphism names for diagnostic purposes;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| Sun, 26 May 2013 19:45:54 +0200 |
haftmann |
more specific structure for registration into theory and dependency onto locale
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:44:08 +0200 |
haftmann |
tuned structure
|
file |
diff |
annotate
|
| Wed, 22 May 2013 22:56:17 +0200 |
haftmann |
interpretation must always operate on the last element in a local theory stack, not on all elements: interpretated facts must disappear after pop from local theory stack, and transfer from last target is not enough
|
file |
diff |
annotate
|
| Wed, 22 May 2013 22:56:17 +0200 |
haftmann |
mark local theory as brittle also after interpretation inside locales;
|
file |
diff |
annotate
|
| Tue, 23 Apr 2013 11:14:50 +0200 |
haftmann |
brittleness stamping for local theories
|
file |
diff |
annotate
|
| Sat, 05 Jan 2013 18:42:29 +0100 |
wenzelm |
less aggressive Assumption.export_term (similar to Generic_Target.abbrev): merely expand local defs and thus allow notation for local fixes;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2013 17:38:54 +0100 |
wenzelm |
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2012 19:43:18 +0200 |
wenzelm |
discontinued complicated/unreliable notion of recent proofs within context;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2012 22:24:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2012 16:35:30 +0200 |
wenzelm |
more precise register_proofs for local goals;
|
file |
diff |
annotate
|
| Mon, 02 Apr 2012 23:27:24 +0200 |
wenzelm |
better restore after close_target;
|
file |
diff |
annotate
|
| Mon, 02 Apr 2012 17:00:32 +0200 |
wenzelm |
better restore to first target, not last target;
|
file |
diff |
annotate
|
| Mon, 02 Apr 2012 15:42:50 +0200 |
wenzelm |
more general Local_Theory.restore, allow any nesting level;
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 18:01:19 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 01 Apr 2012 14:29:22 +0200 |
wenzelm |
Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom;
|
file |
diff |
annotate
|
| Thu, 22 Mar 2012 15:41:49 +0100 |
wenzelm |
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 17:25:35 +0100 |
wenzelm |
basic support for nested contexts including bundles;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 15:19:45 +0100 |
wenzelm |
basic support for nested local theory targets;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 11:25:19 +0100 |
wenzelm |
clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 16:07:03 +0100 |
wenzelm |
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 12:57:43 +0200 |
wenzelm |
uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 22:17:30 +0200 |
wenzelm |
uniform Local_Theory.declaration with explicit params;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
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
|
| Wed, 11 Aug 2010 17:19:27 +0200 |
haftmann |
remove reinit operation alltogether
|
file |
diff |
annotate
|
| Tue, 10 Aug 2010 14:11:28 +0200 |
haftmann |
try to uniformly follow define/note/abbrev/declaration order as close as possible
|
file |
diff |
annotate
|
| Sat, 24 Jul 2010 12:14:53 +0200 |
wenzelm |
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
|
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
|
| Wed, 28 Apr 2010 11:41:27 +0200 |
wenzelm |
localized default sort;
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 19:20:52 +0200 |
wenzelm |
implicit checkpoint in Local_Theory.theory as well -- no longer export Local_Theory.checkpoint;
|
file |
diff |
annotate
|
| Mon, 15 Mar 2010 18:59:16 +0100 |
wenzelm |
replaced type_syntax/term_syntax by uniform syntax_declaration;
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 14:40:36 +0100 |
wenzelm |
added Local_Theory.alias operations (independent of target);
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 17:07:36 +0100 |
wenzelm |
more uniform treatment of syntax for types vs. consts;
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 14:44:22 +0100 |
wenzelm |
Local_Theory.define: eliminated slightly odd kind argument -- such low-level definitions should be hardly ever exposed to end-users anyway;
|
file |
diff |
annotate
|
| Tue, 17 Nov 2009 14:50:55 +0100 |
wenzelm |
uniform new_group/reset_group;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 20:41:29 +0100 |
wenzelm |
eliminated slightly odd kind argument of LocalTheory.note(s);
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 22:06:46 +0100 |
wenzelm |
allow "pervasive" local theory declarations, which are applied the background theory;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:30:40 +0100 |
wenzelm |
modernized structure Context_Position;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 17:36:34 +0100 |
wenzelm |
let naming transform binding beforehand -- covering only the "conceal" flag for now;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 16:25:10 +0100 |
wenzelm |
added restore_naming;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 19:18:25 +0100 |
wenzelm |
maintain proper Name_Space.naming, with conceal and set_group;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 12:27:21 +0100 |
wenzelm |
allow name space entries to be "concealed" -- via binding/naming/local_theory;
|
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
|