src/Pure/Isar/specification.ML
2009-01-21 wenzelm 2009-01-21 removed Ids;
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-19 ballarin 2008-12-19 All logics ported to new locales.
2008-12-05 haftmann 2008-12-05 Name.name_of -> Binding.base_name
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-12-01 haftmann 2008-12-01 new Binding module
2008-11-24 ballarin 2008-11-24 Enable switching to new locales during session.
2008-11-24 ballarin 2008-11-24 More ramifications of removal of 'includes' element.
2008-11-20 haftmann 2008-11-20 tuned name bindings
2008-11-20 wenzelm 2008-11-20 removed traces of former 'includes' element;
2008-11-17 haftmann 2008-11-17 adjusted locale signature to *_cmd convention
2008-11-14 haftmann 2008-11-14 Name.is_nothing
2008-10-30 ballarin 2008-10-30 Dropped context element 'includes'.
2008-10-28 haftmann 2008-10-28 cleanup code default attribute
2008-09-26 haftmann 2008-09-26 removed obsolete name convention "func"
2008-09-03 wenzelm 2008-09-03 axiomatization is now global-only;
2008-09-02 wenzelm 2008-09-02 ProofDisplay.print_results;
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; simplified ProofContext.inferred_param;
2008-08-13 wenzelm 2008-08-13 ProofDisplay.theory_results;
2008-04-09 wenzelm 2008-04-09 print_consts only for external specifications;
2008-03-20 wenzelm 2008-03-20 renamed former get_thms(_silent) to get_fact(_silent);
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2007-11-10 wenzelm 2007-11-10 notation: improved ProofContext.read_const does the job;
2007-10-26 wenzelm 2007-10-26 notation: associate syntax to checked-unchecked term;
2007-10-13 wenzelm 2007-10-13 renamed LocalTheory.def to LocalTheory.define;
2007-10-12 wenzelm 2007-10-12 more informative TheoryTarget.peek operation;
2007-10-11 wenzelm 2007-10-11 removed unused/impure quiet_mode; local_theory: incorporated consts into axioms; tuned;
2007-10-10 wenzelm 2007-10-10 generalized notation interface (add or del);
2007-10-09 wenzelm 2007-10-09 Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
2007-10-04 wenzelm 2007-10-04 replaced literal 'a by Name.aT;
2007-09-26 wenzelm 2007-09-26 read/check_specification: free_dummy_patterns;
2007-09-26 wenzelm 2007-09-26 read/check_specification: proper type inference across multiple sections, result is in closed form; added read/check_free_specification for single section, non-closed form;
2007-09-22 wenzelm 2007-09-22 ProofContext.mode_abbrev;
2007-09-18 haftmann 2007-09-18 distinction between regular and default code theorems
2007-09-07 wenzelm 2007-09-07 theorem: apply hook last;
2007-09-06 wenzelm 2007-09-06 theorem hooks: apply in declaration order;
2007-08-28 wenzelm 2007-08-28 TheoremHook: fixed copy-paste mistake;
2007-08-28 berghofe 2007-08-28 - theorem(_i) now also takes "interactive" flag as argument - added theorem hook
2007-08-10 haftmann 2007-08-10 new structure for code generator modules
2007-05-10 berghofe 2007-05-10 Changed name of raw definition.
2007-04-20 haftmann 2007-04-20 Isar definitions are now added explicitly to code theorem table
2006-12-15 wenzelm 2006-12-15 renamed LocalTheory.assert to affirm;
2006-12-12 wenzelm 2006-12-12 LocalTheory.abbrev;
2006-12-10 wenzelm 2006-12-10 LocalTheory.notation/abbrev;
2006-12-09 wenzelm 2006-12-09 TermSyntax.abbrev; ProofContext.set_expand_abbrevs;
2006-12-07 wenzelm 2006-12-07 definition/abbreviation: single argument;
2006-12-07 wenzelm 2006-12-07 TermSyntax.notation/abbrevs;
2006-12-05 wenzelm 2006-12-05 Attrib.internal: morphism;
2006-11-30 wenzelm 2006-11-30 Goal.norm/close_result;
2006-11-26 wenzelm 2006-11-26 abbrevs: no result; Element.map_ctxt_attrib;
2006-11-21 wenzelm 2006-11-21 theorem(_i): note assms of statement;
2006-11-21 wenzelm 2006-11-21 LocalTheory.axioms/notes/defs: proper kind; simplified Proof.theorem(_i);
2006-11-14 wenzelm 2006-11-14 replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
2006-11-14 wenzelm 2006-11-14 simplified Proof.theorem(_i) interface;
2006-11-09 wenzelm 2006-11-09 abbrevs: return result; LocalTheory.restore;
2006-11-07 wenzelm 2006-11-07 complex goal statements: misc cleanup;
2006-11-07 wenzelm 2006-11-07 theorem statements: incorporate Obtain.statement, tuned;
2006-11-07 wenzelm 2006-11-07 replaced const_syntax by notation, which operates on terms;
2006-10-14 wenzelm 2006-10-14 added theorem(_i);