src/Pure/Isar/generic_target.ML
Tue, 03 Apr 2012 16:49:05 +0200 wenzelm another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix);
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);
Tue, 03 Apr 2012 16:10:34 +0200 wenzelm better drop background syntax if entity depends on parameters;
Tue, 03 Apr 2012 14:37:16 +0200 wenzelm more uniform abbrev vs. define;
Tue, 03 Apr 2012 11:28:21 +0200 wenzelm clarified generic_const vs. close_schematic_term;
Tue, 03 Apr 2012 10:59:20 +0200 wenzelm more uniform theory_abbrev with const_declaration;
Tue, 03 Apr 2012 10:04:41 +0200 wenzelm avoid const_declaration in aux. context (cf. locale_foundation);
Tue, 03 Apr 2012 09:47:20 +0200 wenzelm clarified background_foundation vs. theory_foundation (with const_declaration);
Tue, 03 Apr 2012 09:41:16 +0200 wenzelm tuned;
Mon, 02 Apr 2012 23:55:25 +0200 wenzelm more general standard_declaration;
Mon, 02 Apr 2012 21:52:03 +0200 wenzelm tuned;
Mon, 02 Apr 2012 21:49:27 +0200 wenzelm clarified standard_declaration vs. theory_declaration;
Mon, 02 Apr 2012 19:54:25 +0200 wenzelm tuned;
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);
Sun, 01 Apr 2012 20:36:33 +0200 wenzelm clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
Sun, 01 Apr 2012 19:07:32 +0200 wenzelm added Attrib.global_notes/local_notes/generic_notes convenience;
Sun, 01 Apr 2012 15:23:43 +0200 wenzelm clarified Named_Target.target_declaration: propagate through other levels as well;
Sun, 01 Apr 2012 14:29:22 +0200 wenzelm Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom;
Sat, 31 Mar 2012 19:38:41 +0200 wenzelm tuned;
Sat, 31 Mar 2012 19:09:59 +0200 wenzelm more direct Local_Defs.contract;
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);
Thu, 22 Mar 2012 11:11:51 +0100 wenzelm tuned;
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.;
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;
Tue, 08 Nov 2011 22:22:59 +0100 wenzelm disabled Thm.compress (again) -- costs for building tables tend to be higher than potential benefit;
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);
Mon, 07 Nov 2011 17:00:23 +0100 wenzelm tuned signature -- avoid spurious Thm.mixed_attribute;
Sat, 05 Nov 2011 22:41:25 +0100 wenzelm tuned;
Sat, 05 Nov 2011 22:01:19 +0100 wenzelm misc tuning;
Sun, 30 Oct 2011 22:20:45 +0100 wenzelm removed obsolete argument (cf. aa35859c8741);
Sat, 29 Oct 2011 12:57:43 +0200 wenzelm uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
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;
Wed, 13 Jul 2011 21:44:15 +0200 wenzelm recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
Wed, 27 Apr 2011 17:58:45 +0200 wenzelm reorganized fixes as specialized (global) name space;
Sun, 17 Apr 2011 21:42:47 +0200 wenzelm added Binding.print convenience, which includes quote already;
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;
Fri, 08 Apr 2011 14:20:57 +0200 wenzelm discontinued special treatment of structure Mixfix;
Sun, 13 Mar 2011 22:55:50 +0100 wenzelm tuned headers;
Fri, 17 Dec 2010 17:08:56 +0100 wenzelm renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
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;
Fri, 27 Aug 2010 19:43:28 +0200 wenzelm more careful treatment of context visibility flag wrt. spurious warnings;
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;
Wed, 11 Aug 2010 12:24:24 +0200 haftmann moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
Tue, 10 Aug 2010 15:09:39 +0200 haftmann basic renumbering
Tue, 10 Aug 2010 14:57:58 +0200 haftmann separated type from term parameters
Tue, 10 Aug 2010 14:53:41 +0200 haftmann moved extra_tfrees check for mixfix syntax to Generic_Target
Tue, 10 Aug 2010 14:47:22 +0200 haftmann name and argument grouping tuning
Tue, 10 Aug 2010 14:42:30 +0200 haftmann whitespace tuning
Tue, 10 Aug 2010 14:15:44 +0200 haftmann added generic_target.ML
less more (0) tip