src/Pure/Isar/isar_thy.ML
2000-04-07 ago apply etc.: comments;
2000-03-30 ago let_bind(_i): polymorphic version;
2000-03-26 ago added 'ultimately';
2000-03-23 ago added 'moreover' command;
2000-03-15 ago removed export_chain;
2000-03-14 ago invoke_case: include attributes;
2000-03-13 ago adapted to new PureThy.add_thms etc.;
2000-03-08 ago added invoke_case;
2000-03-06 ago moved use_mltext, use_mltext_theory, use_let, use_setup to context.ML;
2000-02-13 ago apply: observe facts;
2000-02-10 ago add_judgment;
2000-02-08 ago (then_)tac: assert_backward;
2000-02-08 ago added forget_proof;
2000-02-07 ago tuned prefer/defer;
2000-01-28 ago added defer, prefer;
2000-01-05 ago present chapter;
1999-12-22 ago raw_t(e)xt: any proof mode;
1999-10-28 ago improved IsarThy.init_context;
1999-10-27 ago added init_context;
1999-10-26 ago export kill_theory;
1999-10-21 ago end/kill_theory: check_known_thy;
1999-10-14 ago renamed verbatim/verb to text_raw/txt_raw;
1999-10-13 ago use_text writeln;
1999-10-07 ago verbatim / verb markupup commands;
1999-10-05 ago replace add_title by add_header;
1999-10-01 ago added 'obtain' command;
1999-09-30 ago fix_i, local_def_i: typ option;
1999-09-29 ago present sections;
1999-09-26 ago use_mltext: Context.setmp only;
1999-09-23 ago tuned print_result;
1999-09-22 ago present results;
1999-09-07 ago Method.refine_no_facts;
1999-09-04 ago PureThy.have_thmss: "" replaces None;
1999-09-01 ago fix: common constraints;
1999-08-25 ago improved msg;
1999-08-24 ago fixed add_sect etc.;
1999-08-18 ago assume: multiple args;
1999-08-17 ago begin_update_theory;
1999-08-05 ago local goals: after_qed;
1999-08-03 ago tuned;
1999-07-27 ago removed update_context;
1999-07-15 ago improved print_thms;
1999-07-14 ago more marg_comments;
1999-07-12 ago local qeds: print rule;
1999-07-09 ago added local_def(_i);
1999-07-08 ago added export_chain;
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 add_txt;
1999-07-01 ago added with_facts(_i);
1999-06-28 ago added presume command;
1999-06-04 ago added also, finally;
1999-05-26 ago local qeds: pass cond_print_result;
1999-05-25 ago added formal comment arguments almost everywhere (still ignored);
1999-05-21 ago cleaned comments;
1999-05-17 ago Present.begin_theory now needs an additional argument of type
1999-04-30 ago Comment.text;
1999-04-27 ago tuned;
1999-04-23 ago added thus, hence;