src/Pure/Isar/generic_target.ML
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-05-30 wenzelm 2013-05-30 standardized aliases;
2013-05-26 haftmann 2013-05-26 more specific structure for registration into theory and dependency onto locale
2012-04-03 wenzelm 2012-04-03 more robust re-import wrt. non-HHF assumptions;
2012-04-03 wenzelm 2012-04-03 another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix);
2012-04-03 wenzelm 2012-04-03 export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);
2012-04-03 wenzelm 2012-04-03 better drop background syntax if entity depends on parameters; more direct Type_Infer_Context.const_type instead of Syntax.check_term, which expands abbreviations (and potentially more);
2012-04-03 wenzelm 2012-04-03 more uniform abbrev vs. define;
2012-04-03 wenzelm 2012-04-03 clarified generic_const vs. close_schematic_term;
2012-04-03 wenzelm 2012-04-03 more uniform theory_abbrev with const_declaration;
2012-04-03 wenzelm 2012-04-03 avoid const_declaration in aux. context (cf. locale_foundation);
2012-04-03 wenzelm 2012-04-03 clarified background_foundation vs. theory_foundation (with const_declaration);
2012-04-03 wenzelm 2012-04-03 tuned;
2012-04-02 wenzelm 2012-04-02 more general standard_declaration; generic const declaration, which is applied to nested targets (named target only);
2012-04-02 wenzelm 2012-04-02 tuned;
2012-04-02 wenzelm 2012-04-02 clarified standard_declaration vs. theory_declaration;
2012-04-02 wenzelm 2012-04-02 tuned;
2012-04-02 wenzelm 2012-04-02 refined define/abbrev: allow extra fixes in aux. context vs. bottom target (NB: export_term expands defined variables, leaving fixed ones);
2012-04-01 wenzelm 2012-04-01 clarified Generic_Target.notes: always perform Attrib.partial_evaluation; more uniform Generic_Target.theory_notes/locale_notes: apply facts to all target contexts;
2012-04-01 wenzelm 2012-04-01 added Attrib.global_notes/local_notes/generic_notes convenience;
2012-04-01 wenzelm 2012-04-01 clarified Named_Target.target_declaration: propagate through other levels as well; tuned signature;
2012-04-01 wenzelm 2012-04-01 Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom; Local_Theory.target refers to bottom; tuned signature;
2012-03-31 wenzelm 2012-03-31 tuned;
2012-03-31 wenzelm 2012-03-31 more direct Local_Defs.contract; eliminated slightly odd Local_Defs.trans_term/trans_prop;
2012-03-22 wenzelm 2012-03-22 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); uniform treatment of target contexts as invisible; added Local_Theory.standard_form convenience;
2012-03-22 wenzelm 2012-03-22 tuned;
2012-03-17 wenzelm 2012-03-17 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.; actually make "raw_def" internal (cf. 80123a220219);
2012-03-14 wenzelm 2012-03-14 Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
2011-11-08 wenzelm 2011-11-08 disabled Thm.compress (again) -- costs for building tables tend to be higher than potential benefit;
2011-11-08 wenzelm 2011-11-08 more specific treatment of defines/assumes -- avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);
2011-11-07 wenzelm 2011-11-07 tuned signature -- avoid spurious Thm.mixed_attribute;
2011-11-05 wenzelm 2011-11-05 tuned;
2011-11-05 wenzelm 2011-11-05 misc tuning;
2011-10-30 wenzelm 2011-10-30 removed obsolete argument (cf. aa35859c8741);
2011-10-29 wenzelm 2011-10-29 uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
2011-10-28 wenzelm 2011-10-28 refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
2011-07-13 wenzelm 2011-07-13 recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
2011-04-27 wenzelm 2011-04-27 reorganized fixes as specialized (global) name space;
2011-04-17 wenzelm 2011-04-17 added Binding.print convenience, which includes quote already;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-11-28 wenzelm 2010-11-28 superficial tuning;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-08-27 wenzelm 2010-08-27 more careful treatment of context visibility flag wrt. spurious warnings;
2010-08-26 wenzelm 2010-08-26 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;
2010-08-11 haftmann 2010-08-11 moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
2010-08-10 haftmann 2010-08-10 basic renumbering
2010-08-10 haftmann 2010-08-10 separated type from term parameters
2010-08-10 haftmann 2010-08-10 moved extra_tfrees check for mixfix syntax to Generic_Target
2010-08-10 haftmann 2010-08-10 name and argument grouping tuning
2010-08-10 haftmann 2010-08-10 whitespace tuning
2010-08-10 haftmann 2010-08-10 added generic_target.ML