src/Pure/Isar/isar_syn.ML
2006-11-09 wenzelm 2006-11-09 abbrevs: return result;
2006-11-07 wenzelm 2006-11-07 removed obsolete Locale.smart_theorem;
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-10-14 wenzelm 2006-10-14 theorem: added local_theory version;
2006-10-12 wenzelm 2006-10-12 tuned;
2006-10-11 wenzelm 2006-10-11 'context': demand 'begin', support local theory; removed 'undo_end', recovered 'cannot_undo'; tuned Toplevel.begin_local_theory;
2006-10-11 wenzelm 2006-10-11 'end': handle local theory; 'locale': begin local theory;
2006-10-09 wenzelm 2006-10-09 lemmas/theorems/declare: Specification.theorems;
2006-09-30 wenzelm 2006-09-30 added undo_end;
2006-09-19 wenzelm 2006-09-19 'print_theory': bang option for full verbosity;
2006-09-18 wenzelm 2006-09-18 added class_deps;
2006-08-09 wenzelm 2006-08-09 locale interpretation command: after_qed;
2006-08-02 wenzelm 2006-08-02 simplified Proof.end_block;
2006-06-11 wenzelm 2006-06-11 fixes: include mixfix syntax;
2006-06-07 wenzelm 2006-06-07 added 'if' and 'for' keywords; tuned;
2006-05-16 wenzelm 2006-05-16 added 'const_syntax';
2006-05-13 wenzelm 2006-05-13 'defs': unchecked flag;
2006-04-30 wenzelm 2006-04-30 AxClass.define_class; AxClass.axiomatize_class/classrel/arity;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-13 wenzelm 2006-04-13 axclass: old-style concrete syntax for canonical specification format;
2006-04-11 wenzelm 2006-04-11 'axclass': no parameters;
2006-04-08 wenzelm 2006-04-08 'abbreviation': optional print mode;
2006-03-20 ballarin 2006-03-20 Tuned signature of Locale.add_locale(_i).
2006-03-17 ballarin 2006-03-17 add_locale(_i) returns internal locale name.
2006-03-14 wenzelm 2006-03-14 added 'print_statement' command;
2006-03-14 wenzelm 2006-03-14 added 'no_translations';
2006-03-11 wenzelm 2006-03-11 *** empty log message ***
2006-03-08 wenzelm 2006-03-08 constdecl: always allow 'where';
2006-02-16 wenzelm 2006-02-16 added 'abbreviation'; tuned;
2006-02-06 wenzelm 2006-02-06 Toplevel.local_theory;
2006-02-03 haftmann 2006-02-03 refined signature of locale module
2006-02-02 wenzelm 2006-02-02 moved (general_)statement to outer_parse.ML;
2006-01-28 wenzelm 2006-01-28 removed obsolete keyword 'files';
2006-01-27 wenzelm 2006-01-27 moved theorem tags from Drule to PureThy;
2006-01-25 wenzelm 2006-01-25 added 'definition'; 'spezification': optional fixes;
2006-01-24 wenzelm 2006-01-24 axiomatization: optional vars;
2006-01-13 wenzelm 2006-01-13 uniform handling of fixes;
2006-01-07 wenzelm 2006-01-07 added 'axiomatization';
2006-01-04 wenzelm 2006-01-04 Toplevel.forget_proof;
2006-01-03 wenzelm 2006-01-03 added 'using' command;
2005-11-30 wenzelm 2005-11-30 simulaneous 'def';
2005-11-10 wenzelm 2005-11-10 guess: Toplevel.proof;
2005-11-09 wenzelm 2005-11-09 P.context_element, P.locale_element;
2005-10-18 wenzelm 2005-10-18 use simplified Toplevel.proof etc.;
2005-10-15 wenzelm 2005-10-15 added 'guess';
2005-09-20 wenzelm 2005-09-20 removed obsolete thms_containing;
2005-09-14 wenzelm 2005-09-14 hide: added option '(open)';
2005-09-13 wenzelm 2005-09-13 cleanup parsers and interfaces;
2005-09-05 wenzelm 2005-09-05 chapter/section/subsection/subsubsection/text: optional locale specification;
2005-09-02 ballarin 2005-09-02 print_locale omits facts by default
2005-09-01 wenzelm 2005-09-01 renamed 'thms_containing' to 'find_theorems' -- keep old version for the time being;
2005-08-25 haftmann 2005-08-25 add_locale_context(_i) now exporting elements (still some refinements to be done)
2005-08-24 ballarin 2005-08-24 Printing of interpretations: option to show witness theorems;
2005-08-18 wenzelm 2005-08-18 various Toplevel.theory_context commands: proper presentation in context; simplified interfaces Proof vs. IsarThy;
2005-08-16 wenzelm 2005-08-16 default tags for theory/proof/ML commands; added '%' keyword;
2005-07-14 wenzelm 2005-07-14 type-safe 'oracle' command;
2005-07-13 wenzelm 2005-07-13 Toplevel.actual_proof;
2005-07-07 ballarin 2005-07-07 Preparations for interpretation of locales in locales.
2005-06-29 wenzelm 2005-06-29 cond_print for end-of-proof and calculational commands;
2005-06-17 wenzelm 2005-06-17 Theory.add_typedecls; Sign.local_path;