src/Pure/Isar/isar_thy.ML
2000-05-24 wenzelm 2000-05-24 added "done" proof;
2000-05-21 wenzelm 2000-05-21 adapted to inner syntax of sorts;
2000-05-18 wenzelm 2000-05-18 hide: check declared;
2000-05-18 wenzelm 2000-05-18 'apply' consumes facts;
2000-05-05 wenzelm 2000-05-05 GPLed; improved begin_theory ('files' may change theory);
2000-04-17 wenzelm 2000-04-17 made SML/NJ happy;
2000-04-17 wenzelm 2000-04-17 global/local_path: comment; added name space hide;
2000-04-07 wenzelm 2000-04-07 apply etc.: comments;
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-15 wenzelm 2000-03-15 removed export_chain;
2000-03-14 wenzelm 2000-03-14 invoke_case: include attributes;
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.;
2000-03-08 wenzelm 2000-03-08 added invoke_case;
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 apply: observe facts; apply_end;
2000-02-10 wenzelm 2000-02-10 add_judgment;
2000-02-08 wenzelm 2000-02-08 (then_)tac: assert_backward;
2000-02-08 wenzelm 2000-02-08 added forget_proof;
2000-02-07 wenzelm 2000-02-07 tuned prefer/defer;
2000-01-28 wenzelm 2000-01-28 added defer, prefer;
2000-01-05 wenzelm 2000-01-05 present chapter; tuned proof markup commands; moved obtain to obtain.ML;
1999-12-22 wenzelm 1999-12-22 raw_t(e)xt: any proof mode;
1999-10-28 wenzelm 1999-10-28 improved IsarThy.init_context;
1999-10-27 wenzelm 1999-10-27 added init_context;
1999-10-26 wenzelm 1999-10-26 export kill_theory;
1999-10-21 wenzelm 1999-10-21 end/kill_theory: check_known_thy;
1999-10-14 wenzelm 1999-10-14 renamed verbatim/verb to text_raw/txt_raw;
1999-10-13 wenzelm 1999-10-13 use_text writeln;
1999-10-07 wenzelm 1999-10-07 verbatim / verb markupup commands;
1999-10-05 wenzelm 1999-10-05 replace add_title by add_header;
1999-10-01 wenzelm 1999-10-01 added 'obtain' command;
1999-09-30 wenzelm 1999-09-30 fix_i, local_def_i: typ option;
1999-09-29 wenzelm 1999-09-29 present sections;
1999-09-26 wenzelm 1999-09-26 use_mltext: Context.setmp only; use_mltext(_theory): verbose if int;
1999-09-23 wenzelm 1999-09-23 tuned print_result;
1999-09-22 wenzelm 1999-09-22 present results;
1999-09-07 wenzelm 1999-09-07 Method.refine_no_facts;
1999-09-04 wenzelm 1999-09-04 PureThy.have_thmss: "" replaces None;
1999-09-01 wenzelm 1999-09-01 fix: common constraints; cond_print_calc: Proof.pretty_thm;
1999-08-25 wenzelm 1999-08-25 improved msg;
1999-08-24 wenzelm 1999-08-24 fixed add_sect etc.;
1999-08-18 wenzelm 1999-08-18 assume: multiple args;
1999-08-17 wenzelm 1999-08-17 begin_update_theory;
1999-08-05 wenzelm 1999-08-05 local goals: after_qed;
1999-08-03 wenzelm 1999-08-03 tuned; added sect, subsect, subsubsect;
1999-07-27 wenzelm 1999-07-27 removed update_context; context / theory: proper update in interactive mode;
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 local qeds: print rule;
1999-07-09 wenzelm 1999-07-09 added local_def(_i); removed global_qed_with(_i);
1999-07-08 wenzelm 1999-07-08 added export_chain; propp: 'concl' patterns; terminal_proof: 2nd method; use Display.pretty_thm_no_hyps;
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 add_txt;
1999-07-01 wenzelm 1999-07-01 added with_facts(_i); also, finally: opt_rules;
1999-06-28 wenzelm 1999-06-28 added presume command;
1999-06-04 wenzelm 1999-06-04 added also, finally;