src/Pure/Isar/isar_syn.ML
2000-05-24 wenzelm 2000-05-24 added "done" proof;
2000-05-21 wenzelm 2000-05-21 replaced {{ }} by { };
2000-05-18 wenzelm 2000-05-18 print_state: flag for proof only;
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-04-17 wenzelm 2000-04-17 added 'hide';
2000-04-07 wenzelm 2000-04-07 apply etc.: comments;
2000-04-06 wenzelm 2000-04-06 'welcome' made diagnostic;
2000-04-05 wenzelm 2000-04-05 removed "as" keyword;
2000-04-03 wenzelm 2000-04-03 markup_env_command 'text' / 'txt';
2000-04-01 wenzelm 2000-04-01 'cd': diag;
2000-03-30 wenzelm 2000-03-30 let_bind(_i): polymorphic version;
2000-03-26 wenzelm 2000-03-26 added 'ultimately';
2000-03-23 wenzelm 2000-03-23 added 'moreover' command;
2000-03-18 wenzelm 2000-03-18 'oops' made proper; removed 'kill_proof' (superceded by 'kill');
2000-03-17 wenzelm 2000-03-17 generic "kill" command;
2000-03-15 wenzelm 2000-03-15 'pr': modes, optional limit; 'thm' / 'prop' / 'term' / 'typ': modes; removed 'thence';
2000-03-14 wenzelm 2000-03-14 'undo' prints state (again); 'pr' command: optional limit argument;
2000-03-14 wenzelm 2000-03-14 invoke_case: include attributes;
2000-03-08 wenzelm 2000-03-08 added 'case' command; added 'print_cases' command;
2000-03-06 wenzelm 2000-03-06 moved use_mltext, use_mltext_theory, use_let, use_setup to context.ML;
2000-02-13 wenzelm 2000-02-13 prf_script commands made proper; removed then_apply; added apply_end;
2000-02-10 wenzelm 2000-02-10 add_judgment;
2000-02-08 wenzelm 2000-02-08 added forget_proof;
2000-01-28 wenzelm 2000-01-28 added defer, prefer;
2000-01-05 wenzelm 2000-01-05 moved obtain to obtain.ML;
1999-10-26 wenzelm 1999-10-26 added kill_thy;
1999-10-21 wenzelm 1999-10-21 added touch_child_thys;
1999-10-20 wenzelm 1999-10-20 use_mltext: better control of verbosity;
1999-10-20 wenzelm 1999-10-20 fixed update_thy_only;
1999-10-14 wenzelm 1999-10-14 renamed verbatim/verb to text_raw/txt_raw;
1999-10-07 wenzelm 1999-10-07 verbatim markup tokens;
1999-10-07 wenzelm 1999-10-07 verbatim / verb markupup commands;
1999-10-06 wenzelm 1999-10-06 OuterSyntax.markup_command;
1999-10-05 wenzelm 1999-10-05 clear_undo replaced by clear_undos; title replaced by header;
1999-10-01 wenzelm 1999-10-01 added 'obtain' command;
1999-09-26 wenzelm 1999-09-26 added 'thms_containing', 'ML_setup';
1999-09-25 wenzelm 1999-09-25 defs: name mandatory;
1999-09-03 wenzelm 1999-09-03 added welcome;
1999-09-01 wenzelm 1999-09-01 replaced IsarCmd.kill_theory by Toplevel.kill; fix: common constraints; removed "*" keyword;
1999-08-26 wenzelm 1999-08-26 improved back, help;
1999-08-20 wenzelm 1999-08-20 print_context;
1999-08-18 wenzelm 1999-08-18 assume/presume: and_list1;
1999-08-16 wenzelm 1999-08-16 disable_pr, enable_pr;
1999-08-09 wenzelm 1999-08-09 pr / no_pr: maintain Toplevel.quiet;
1999-08-03 wenzelm 1999-08-03 tuned; added sect, subsect, subsubsect;
1999-07-30 wenzelm 1999-07-30 oracle: '=';
1999-07-28 wenzelm 1999-07-28 added pretty_setmargin;
1999-07-27 wenzelm 1999-07-27 removed update_context; removed restart; added init_toplevel, touch_all_thys, touch_thy, remove_thy, update_thy_only;
1999-07-16 wenzelm 1999-07-16 removed break;
1999-07-15 wenzelm 1999-07-15 improved print_thms;
1999-07-14 wenzelm 1999-07-14 more marg_comments;
1999-07-12 wenzelm 1999-07-12 def: ==;
1999-07-09 wenzelm 1999-07-09 added 'def'; added "!!" keyword; removed 'qed_with';
1999-07-08 wenzelm 1999-07-08 propp: 'concl' patterns; added 'thence';
1999-07-06 wenzelm 1999-07-06 removed proof history nesting commands (not useful);
1999-07-03 wenzelm 1999-07-03 fixed 'txt';
1999-07-02 wenzelm 1999-07-02 skip_proof feature 'sorry' (for quick_and_dirty mode only);
1999-07-02 wenzelm 1999-07-02 added 'txt';
1999-07-01 wenzelm 1999-07-01 'with' as == 'from' as facts; also, finally: opt_rules;
1999-07-01 wenzelm 1999-07-01 fix, assume, presume: prf_asm;