src/Pure/Isar/isar_thy.ML
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;
1998-11-09 ago Derived theory operations.