src/Pure/Isar/isar_thy.ML
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;
1999-04-22 ago switch_theory: Context.pass;
1999-03-19 ago common qed and end of proofs;
1999-03-17 ago added '_i' versions;
1999-03-11 ago add_title;
1999-03-09 ago begin/end_theory: presentation;
1999-02-08 ago Context.fetch, Context.setmp;
1999-02-05 ago made MLWorks happy;
1999-02-05 ago improved theory, context, update_context;
1999-02-03 ago ThyInfo.begin_theory;
1999-01-12 ago 'same' method, 'immediate' proof;
1999-01-12 ago eliminated tthm type and Attribute structure;
1998-11-25 ago add_text, add_chapter etc.: dummy;
1998-11-19 ago match_bind: 'as' patterns;
1998-11-18 ago tuned comments;
1998-11-17 ago added have_theorems, have_lemmas, have_facts;
1998-11-16 ago renamed tac / etac to refine / then_refine;