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;
2006-02-16 ago added abbrev element;
2006-02-15 ago init/exit no longer change the theory (no naming);
2006-02-12 ago tuned;
2006-02-11 ago added restore;
2006-02-06 ago type local_theory = Proof.context;
2006-01-31 ago added consts_retricted;
2006-01-28 ago added print_consts;