src/Pure/Isar/specification.ML
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.