src/Pure/Isar/isar_syn.ML
2000-09-01 wenzelm 2000-09-01 'declare' made proper command;
2000-08-29 wenzelm 2000-08-29 pr: added prems limit;
2000-08-14 wenzelm 2000-08-14 added "declare" command;
2000-08-08 wenzelm 2000-08-08 prf_heading kind;
2000-07-30 wenzelm 2000-07-30 def: no constraint on var;
2000-07-27 wenzelm 2000-07-27 added thm_deps;
2000-07-13 wenzelm 2000-07-13 defs: (overloaded) option;
2000-07-06 wenzelm 2000-07-06 allow comment in more commands;
2000-07-01 wenzelm 2000-07-01 removed "help"; added "print_commands", "print_trans_rules", "print_antiquotations";
2000-06-29 wenzelm 2000-06-29 added method_setup; facts: handle multiple lists of arguments;
2000-06-25 wenzelm 2000-06-25 use ThyHeader.args; adapted OuterSyntax.markup_command;
2000-06-08 wenzelm 2000-06-08 prf_open/close;
2000-06-04 wenzelm 2000-06-04 opt_mixfix', opt_infix';
2000-06-03 wenzelm 2000-06-03 block commands: marginal comment;
2000-05-31 wenzelm 2000-05-31 Toplevel.no_timing;
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;