src/Pure/Isar/specification.ML
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);
2006-10-09 wenzelm 2006-10-09 added theorems(_i) -- with present_results;
2006-10-07 wenzelm 2006-10-07 moved pretty_consts to proof_display.ML; adapted to improved LocalTheory interfaces;
2006-09-29 wenzelm 2006-09-29 Syntax.mode;
2006-05-16 wenzelm 2006-05-16 added const_syntax(_i);
2006-05-07 wenzelm 2006-05-07 removed 'concl is' patterns;
2006-05-02 wenzelm 2006-05-02 abbreviation: observe local syntax mode;
2006-04-08 wenzelm 2006-04-08 abbreviation(_i): do not expand abbreviations, do not use derived_def;
2006-02-16 wenzelm 2006-02-16 added abbreviation(_i);
2006-02-06 wenzelm 2006-02-06 type local_theory; removed _loc versions;
2006-01-31 wenzelm 2006-01-31 axiomatization: retrict parameters to occurrences in specs; definition: restrict parameters to individual rhs;
2006-01-28 wenzelm 2006-01-28 added axiomatization_loc, definition_loc; definition: let LocalDefs.derived_def do the actual work;
2006-01-27 wenzelm 2006-01-27 swapped Toplevel.theory_context; definition(_i): actually rulify as well, support more of object-logic; definition(_i): more precise treatment of local fixes;
2006-01-25 wenzelm 2006-01-25 added definition(_i);
2006-01-24 wenzelm 2006-01-24 renamed axiomatize(_i) to axiomatization(_i); LocalTheory;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-13 wenzelm 2006-01-13 uniform handling of fixes;
2006-01-10 wenzelm 2006-01-10 generic attributes; tuned;
2006-01-07 wenzelm 2006-01-07 Theory specifications --- with type-inference, but no internal polymorphism.