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.