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