2013-05-22 haftmann 2013-05-22 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
2013-05-22 haftmann 2013-05-22 mark local theory as brittle also after interpretation inside locales; more correct bookkeeping on brittleness: must store directly beside lthy data, with implicit default true for levels > 1; check brittleness only during context switch using (in ...) syntax, not for arbitrary exit of local theory
2013-04-23 haftmann 2013-04-23 brittleness stamping for local theories
2013-01-05 wenzelm 2013-01-05 less aggressive Assumption.export_term (similar to Generic_Target.abbrev): merely expand local defs and thus allow notation for local fixes;
2013-01-05 wenzelm 2013-01-05 more precise Local_Theory.level: 1 really means main target and >= 2 nested context; explicit target for context within global theory with after_close = exit to manage the 2 levels involved here; reject "(in target)" for nested contexts more reliably -- difficult to handle due to lack of nested reinit;
2012-09-01 wenzelm 2012-09-01 discontinued complicated/unreliable notion of recent proofs within context;
2012-08-31 wenzelm 2012-08-31 tuned signature;
2012-08-31 wenzelm 2012-08-31 more precise register_proofs for local goals; tuned signature;
2012-04-02 wenzelm 2012-04-02 better restore after close_target;
2012-04-02 wenzelm 2012-04-02 better restore to first target, not last target;
2012-04-02 wenzelm 2012-04-02 more general Local_Theory.restore, allow any nesting level;
2012-04-01 wenzelm 2012-04-01 tuned signature;
2012-04-01 wenzelm 2012-04-01 Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom; refers to bottom; tuned signature;
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-21 wenzelm 2012-03-21 basic support for nested contexts including bundles; include multiple bundles; renamed "affirm" back to "assert" (cf. c4492c6bf450 which was motivated by obsolete Alice/ML); tuned signatures;
2012-03-21 wenzelm 2012-03-21 basic support for nested local theory targets;
2012-03-21 wenzelm 2012-03-21 clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2); 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);
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 uniform Local_Theory.declaration with explicit params;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
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-26 wenzelm 2010-08-26 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;
2010-08-11 haftmann 2010-08-11 remove reinit operation alltogether
2010-08-10 haftmann 2010-08-10 try to uniformly follow define/note/abbrev/declaration order as close as possible
2010-07-24 wenzelm 2010-07-24 moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state; theory loader: reduced warnings -- thy database can be bypassed in certain situations; Proof/Local_Theory.propagate_ml_env; ML use function: propagate ML environment as well; pervasive type generic_theory;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-28 wenzelm 2010-04-28 localized default sort;
2010-03-28 wenzelm 2010-03-28 implicit checkpoint in Local_Theory.theory as well -- no longer export Local_Theory.checkpoint;
2010-03-15 wenzelm 2010-03-15 replaced type_syntax/term_syntax by uniform syntax_declaration;
2010-03-13 wenzelm 2010-03-13 added Local_Theory.alias operations (independent of target);
2010-03-01 wenzelm 2010-03-01 more uniform treatment of syntax for types vs. consts;
2009-11-19 wenzelm 2009-11-19 Local_Theory.define: eliminated slightly odd kind argument -- such low-level definitions should be hardly ever exposed to end-users anyway;
2009-11-17 wenzelm 2009-11-17 uniform new_group/reset_group; tuned signature;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-13 wenzelm 2009-11-13 eliminated slightly odd kind argument of LocalTheory.note(s); added LocalTheory.notes_kind as fall-back for unusual cases;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-05 wenzelm 2009-11-05 allow "pervasive" local theory declarations, which are applied the background theory;
2009-11-02 wenzelm 2009-11-02 modernized structure Context_Position;
2009-10-28 wenzelm 2009-10-28 let naming transform binding beforehand -- covering only the "conceal" flag for now; export LocalTheory.standard_morphism;
2009-10-28 wenzelm 2009-10-28 added restore_naming;
2009-10-25 wenzelm 2009-10-25 maintain proper Name_Space.naming, with conceal and set_group; maintain group via name space, not tags; tuned signature; tuned;
2009-10-25 wenzelm 2009-10-25 allow name space entries to be "concealed" -- via binding/naming/local_theory;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-03-19 wenzelm 2009-03-19 added map_contexts (cf. Proof.map_contexts);
2009-03-12 wenzelm 2009-03-12 renamed sticky_prefix to mandatory_path;
2009-03-11 wenzelm 2009-03-11 eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-17 haftmann 2008-12-17 dropped Ids
2008-12-05 haftmann 2008-12-05 dropped NameSpace.declare_base
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-09-29 wenzelm 2008-09-29 target update: invisible context position avoids duplication of reports etc.;
2008-09-29 wenzelm 2008-09-29 added exit_global, exit_result, exit_result_global; ProofContext.norm_export_morphism;
2008-09-27 wenzelm 2008-09-27 Theory.checkpoint for main operations, admits concurrent proofs;
2008-09-03 wenzelm 2008-09-03 discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
2008-09-02 wenzelm 2008-09-02 type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-08-27 wenzelm 2008-08-27 type Properties.T;
2008-02-25 wenzelm 2008-02-25 maintain group in lthy data, implicit use in operations; tuned signature; added group_position_of;
2008-01-26 wenzelm 2008-01-26 grouped versions of axioms/define/notes;