src/Pure/Isar/isar_syn.ML
2007-08-24 haftmann 2007-08-24 overloaded definitions accompanied by explicit constants
2007-08-17 wenzelm 2007-08-17 removed obsolete touch_all_thys;
2007-08-10 haftmann 2007-08-10 new structure for code generator modules
2007-08-07 wenzelm 2007-08-07 theory loader: removed obsolete update_thy (coincides with use_thy);
2007-08-01 wenzelm 2007-08-01 renamed 'print_options' to 'print_configs';
2007-07-25 wenzelm 2007-07-25 added command 'print_options';
2007-07-19 wenzelm 2007-07-19 removed obsolete use/update_thy_only;
2007-07-12 wenzelm 2007-07-12 command 'declare': proper thy_decl;
2007-05-08 wenzelm 2007-05-08 tuned;
2007-04-26 wenzelm 2007-04-26 renamed some old names Theory.xxx to Sign.xxx;
2007-04-20 haftmann 2007-04-20 Isar definitions are now added explicitly to code theorem table
2007-04-03 wenzelm 2007-04-03 avoid clash with Alice keywords;
2007-03-20 haftmann 2007-03-20 added theory dependency graph
2007-03-06 kleing 2007-03-06 fix wrong default for find_theorems
2007-03-06 kleing 2007-03-06 find_theorems: moved with_dup into the brackets, i.e. find_theorems (20 with_dups) "some term" ..
2007-03-02 haftmann 2007-03-02 syntax for "class attach const"
2007-02-23 haftmann 2007-02-23 locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
2007-02-20 kleing 2007-02-20 Remove duplicates from printed theorems in find_theorems (still pretty slow, needs optimising). Added syntax "find_theorems (..) with_dups .." to switch off removal.
2007-02-16 wenzelm 2007-02-16 unified arity parser/arguments;
2007-02-14 haftmann 2007-02-14 class package now using Locale.interpretation_i
2007-02-10 haftmann 2007-02-10 moved commands of class package here
2007-02-04 wenzelm 2007-02-04 tuned oracle interface; simproc_setup: added identifier;
2007-01-28 wenzelm 2007-01-28 added simproc_setup;
2007-01-19 wenzelm 2007-01-19 renamed IsarOutput to ThyOutput; moved parts of OuterParse to SpecParse; renamed OuterParse locale_target to target;
2007-01-19 wenzelm 2007-01-19 added 'declaration' command;
2006-12-30 wenzelm 2006-12-30 removed obsolete 'clear_undos';
2006-12-29 haftmann 2006-12-29 changed syntax for axclass attach
2006-12-14 wenzelm 2006-12-14 locale: print context for begin;
2006-12-12 wenzelm 2006-12-12 classified show/thus as prf_asm_goal, which is usually hilited in PG;
2006-12-09 wenzelm 2006-12-09 added 'print_abbrevs';
2006-12-08 wenzelm 2006-12-08 added 'help' command (same of 'print_commands');
2006-12-07 wenzelm 2006-12-07 definition/abbreviation: single argument;
2006-11-30 wenzelm 2006-11-30 simplified syntax for 'definition', 'abbreviation';
2006-11-26 wenzelm 2006-11-26 abbrevs: no result;
2006-11-22 haftmann 2006-11-22 added Isar syntax for adding parameters to axclasses
2006-11-21 wenzelm 2006-11-21 moved theorem kinds from PureThy to Thm;
2006-11-17 wenzelm 2006-11-17 'notation': more robust 'and' list;
2006-11-14 wenzelm 2006-11-14 incorporated IsarThy into IsarCmd;
2006-11-11 wenzelm 2006-11-11 turned 'context' into plain thy_decl, discontinued thy_switch;
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;