src/Pure/Isar/local_theory.ML
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;
2006-02-15 wenzelm 2006-02-15 init/exit no longer change the theory (no naming); added naming, restore_naming, mapping;
2006-02-12 wenzelm 2006-02-12 tuned;
2006-02-11 wenzelm 2006-02-11 added restore; consts: provide abbreviations;
2006-02-06 wenzelm 2006-02-06 type local_theory = Proof.context; print_consts: subject to quiet_mode;
2006-01-31 wenzelm 2006-01-31 added consts_retricted; pretty/print_consts: parameter restriction;
2006-01-28 wenzelm 2006-01-28 added print_consts; tuned;
2006-01-27 wenzelm 2006-01-27 improved 'notes', including proper treatment of locale results; tuned;
2006-01-25 wenzelm 2006-01-25 added constant definition; tuned interfaces; tuned;
2006-01-24 wenzelm 2006-01-24 added actual operations;
2006-01-22 wenzelm 2006-01-22 Local theory operations, with optional target locale.