src/Pure/Isar/local_theory.ML
2009-03-11 ago 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 ago binding is alias for Binding.T
2008-12-17 ago dropped Ids
2008-12-05 ago dropped NameSpace.declare_base
2008-12-04 ago cleaned up binding module and related code
2008-09-29 ago target update: invisible context position avoids duplication of reports etc.;
2008-09-29 ago added exit_global, exit_result, exit_result_global;
2008-09-27 ago Theory.checkpoint for main operations, admits concurrent proofs;
2008-09-03 ago discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
2008-09-02 ago type Attrib.binding abbreviates Name.binding without attributes;
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-08-27 ago type Properties.T;
2008-02-25 ago maintain group in lthy data, implicit use in operations;
2008-01-26 ago grouped versions of axioms/define/notes;
2007-11-10 ago removed LocalTheory.target_naming/name;
2007-11-05 ago simplified LocalTheory.reinit;
2007-10-20 ago tuned abbrev interface;
2007-10-19 ago tuned interfaces;
2007-10-14 ago tuned;
2007-10-13 ago renamed def to define;
2007-10-11 ago local_theory: incorporated consts into axioms;
2007-10-10 ago generalized notation interface (add or del);
2007-10-09 ago removed LocalTheory.defs/target_morphism operations;
2007-09-07 ago fixed type alias in signature;
2007-07-28 ago type Morphism.declaration;
2007-07-28 ago tuned signature;
2007-05-07 ago simplified DataFun interfaces;
2007-02-04 ago added full_naming;
2007-01-28 ago added interface for target_naming;
2006-12-15 ago renamed LocalTheory.assert to affirm;
2006-12-12 ago abbrev: tuned signature;
2006-12-10 ago added notation/abbrev (from term_syntax.ML);
2006-12-07 ago moved notation/abbrevs to TermSyntax;
2006-12-06 ago abbrevs: actually observe target_morphism;
2006-12-05 ago notation/abbreviation: more serious handling of morphisms;
2006-11-30 ago added full_name;
2006-11-26 ago abbrevs: no result;
2006-11-23 ago uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
2006-11-21 ago LocalTheory.axioms/notes/defs: proper kind;
2006-11-10 ago simplified exit;
2006-11-09 ago abbrevs: return result;
2006-11-07 ago replaced const_syntax by notation, which operates on terms;
2006-10-14 ago added assert;
2006-10-11 ago exit: pass interactive flag, toplevel result convention;
2006-10-11 ago added raw_theory(_result);
2006-10-09 ago added exit;
2006-10-07 ago turned into abstract wrapper module, cf. theory_target.ML;
2006-09-29 ago Syntax.mode;
2006-09-28 ago Sign.add_consts_authentic;
2006-07-29 ago tuned comment;
2006-07-27 ago renamed ProofContext.fix_frees to Variable.fix_frees;
2006-07-27 ago "moved basic assumption operations from structure ProofContext to Assumption;"
2006-07-06 ago removed obsolete locale view;
2006-07-04 ago Locales no longer generate views. The following functions have changed
2006-06-17 ago standard: simultaneous facts;
2006-05-17 ago export generic term_syntax;
2006-05-16 ago added syntax interface;
2006-05-13 ago Theory.add_defs(_i): added unchecked flag;
2006-04-30 ago tuned;
2006-04-08 ago abbrevs: support print mode;