src/Pure/Isar/local_theory.ML
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;
2007-11-10 wenzelm 2007-11-10 removed LocalTheory.target_naming/name;
2007-11-05 wenzelm 2007-11-05 simplified LocalTheory.reinit;
2007-10-20 wenzelm 2007-10-20 tuned abbrev interface;
2007-10-19 wenzelm 2007-10-19 tuned interfaces;
2007-10-14 wenzelm 2007-10-14 tuned;
2007-10-13 wenzelm 2007-10-13 renamed def to define; abbrev: return hypothetical def;
2007-10-11 wenzelm 2007-10-11 local_theory: incorporated consts into axioms;
2007-10-10 wenzelm 2007-10-10 generalized notation interface (add or del);
2007-10-09 wenzelm 2007-10-09 removed LocalTheory.defs/target_morphism operations; added target_morphism (from theory_target.ML);
2007-09-07 wenzelm 2007-09-07 fixed type alias in signature;
2007-07-28 wenzelm 2007-07-28 type Morphism.declaration;
2007-07-28 wenzelm 2007-07-28 tuned signature;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-02-04 wenzelm 2007-02-04 added full_naming;
2007-01-28 wenzelm 2007-01-28 added interface for target_naming;
2006-12-15 wenzelm 2006-12-15 renamed LocalTheory.assert to affirm;
2006-12-12 wenzelm 2006-12-12 abbrev: tuned signature;
2006-12-10 wenzelm 2006-12-10 added notation/abbrev (from term_syntax.ML);
2006-12-07 wenzelm 2006-12-07 moved notation/abbrevs to TermSyntax;
2006-12-06 wenzelm 2006-12-06 abbrevs: actually observe target_morphism;
2006-12-05 wenzelm 2006-12-05 notation/abbreviation: more serious handling of morphisms;
2006-11-30 wenzelm 2006-11-30 added full_name;
2006-11-26 wenzelm 2006-11-26 abbrevs: no result; added target_morphism/name; simplified theory prefix (no option); proper morphing of abbrevs/notation;
2006-11-23 wenzelm 2006-11-23 uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
2006-11-21 wenzelm 2006-11-21 LocalTheory.axioms/notes/defs: proper kind; context_notes: ProofContext.set_stmt after import;
2006-11-10 wenzelm 2006-11-10 simplified exit; added reinit;
2006-11-09 wenzelm 2006-11-09 abbrevs: return result; separate reinit/restore;
2006-11-07 wenzelm 2006-11-07 replaced const_syntax by notation, which operates on terms;
2006-10-14 wenzelm 2006-10-14 added assert;
2006-10-11 wenzelm 2006-10-11 exit: pass interactive flag, toplevel result convention;
2006-10-11 wenzelm 2006-10-11 added raw_theory(_result); tuned;
2006-10-09 wenzelm 2006-10-09 added exit;
2006-10-07 wenzelm 2006-10-07 turned into abstract wrapper module, cf. theory_target.ML; simplified interfaces;
2006-09-29 wenzelm 2006-09-29 Syntax.mode;
2006-09-28 wenzelm 2006-09-28 Sign.add_consts_authentic;
2006-07-29 wenzelm 2006-07-29 tuned comment;
2006-07-27 wenzelm 2006-07-27 renamed ProofContext.fix_frees to Variable.fix_frees;
2006-07-27 wenzelm 2006-07-27 "moved basic assumption operations from structure ProofContext to Assumption;"
2006-07-06 wenzelm 2006-07-06 removed obsolete locale view;
2006-07-04 ballarin 2006-07-04 Locales no longer generate views. The following functions have changed signatures: Locale.init, Locale.add_thmss, Locale.read/cert_context_statement.
2006-06-17 wenzelm 2006-06-17 standard: simultaneous facts;
2006-05-17 wenzelm 2006-05-17 export generic term_syntax;
2006-05-16 wenzelm 2006-05-16 added syntax interface; tuned interface;
2006-05-13 wenzelm 2006-05-13 Theory.add_defs(_i): added unchecked flag;
2006-04-30 wenzelm 2006-04-30 tuned;
2006-04-08 wenzelm 2006-04-08 abbrevs: support print mode;
2006-02-16 wenzelm 2006-02-16 added abbrev element;