Mon, 02 Apr 2012 23:55:25 +0200 |
wenzelm |
more general standard_declaration;
|
file |
diff |
annotate
|
Mon, 02 Apr 2012 21:52:03 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 02 Apr 2012 21:49:27 +0200 |
wenzelm |
clarified standard_declaration vs. theory_declaration;
|
file |
diff |
annotate
|
Mon, 02 Apr 2012 19:54:25 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 02 Apr 2012 16:35:09 +0200 |
wenzelm |
refined define/abbrev: allow extra fixes in aux. context vs. bottom target (NB: export_term expands defined variables, leaving fixed ones);
|
file |
diff |
annotate
|
Sun, 01 Apr 2012 20:36:33 +0200 |
wenzelm |
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
|
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, 01 Apr 2012 14:29:22 +0200 |
wenzelm |
Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom;
|
file |
diff |
annotate
|
Sat, 31 Mar 2012 19:38:41 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 31 Mar 2012 19:09:59 +0200 |
wenzelm |
more direct Local_Defs.contract;
|
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
|
Thu, 22 Mar 2012 11:11:51 +0100 |
wenzelm |
tuned;
|
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
|
Wed, 14 Mar 2012 11:45:16 +0100 |
wenzelm |
Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
|
file |
diff |
annotate
|
Tue, 08 Nov 2011 22:22:59 +0100 |
wenzelm |
disabled Thm.compress (again) -- costs for building tables tend to be higher than potential benefit;
|
file |
diff |
annotate
|
Tue, 08 Nov 2011 15:03:11 +0100 |
wenzelm |
more specific treatment of defines/assumes -- avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);
|
file |
diff |
annotate
|
Mon, 07 Nov 2011 17:00:23 +0100 |
wenzelm |
tuned signature -- avoid spurious Thm.mixed_attribute;
|
file |
diff |
annotate
|
Sat, 05 Nov 2011 22:41:25 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 05 Nov 2011 22:01:19 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
Sun, 30 Oct 2011 22:20:45 +0100 |
wenzelm |
removed obsolete argument (cf. aa35859c8741);
|
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 23:16:50 +0200 |
wenzelm |
refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
|
file |
diff |
annotate
|
Wed, 13 Jul 2011 21:44:15 +0200 |
wenzelm |
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
|
file |
diff |
annotate
|
Wed, 27 Apr 2011 17:58:45 +0200 |
wenzelm |
reorganized fixes as specialized (global) name space;
|
file |
diff |
annotate
|
Sun, 17 Apr 2011 21:42:47 +0200 |
wenzelm |
added Binding.print convenience, which includes quote already;
|
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
|
Fri, 08 Apr 2011 14:20:57 +0200 |
wenzelm |
discontinued special treatment of structure Mixfix;
|
file |
diff |
annotate
|
Sun, 13 Mar 2011 22:55:50 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|