| Tue, 03 Apr 2012 19:49:14 +0200 |
wenzelm |
more robust re-import wrt. non-HHF assumptions;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 16:49:05 +0200 |
wenzelm |
another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix);
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 16:27:32 +0200 |
wenzelm |
export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 16:10:34 +0200 |
wenzelm |
better drop background syntax if entity depends on parameters;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 14:37:16 +0200 |
wenzelm |
more uniform abbrev vs. define;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 11:28:21 +0200 |
wenzelm |
clarified generic_const vs. close_schematic_term;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 10:59:20 +0200 |
wenzelm |
more uniform theory_abbrev with const_declaration;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 10:04:41 +0200 |
wenzelm |
avoid const_declaration in aux. context (cf. locale_foundation);
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 09:47:20 +0200 |
wenzelm |
clarified background_foundation vs. theory_foundation (with const_declaration);
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 09:41:16 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 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
|