src/Pure/Isar/isar_thy.ML
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;
1999-05-26 wenzelm 1999-05-26 local qeds: pass cond_print_result;
1999-05-25 wenzelm 1999-05-25 added formal comment arguments almost everywhere (still ignored);
1999-05-21 wenzelm 1999-05-21 cleaned comments; global statements: init history according to interactive mode; local qed: pass interactive mode; init theory: kill operation;
1999-05-17 berghofe 1999-05-17 Present.begin_theory now needs an additional argument of type theory to store information about session identifiers.
1999-04-30 wenzelm 1999-04-30 Comment.text;
1999-04-27 wenzelm 1999-04-27 tuned;
1999-04-23 wenzelm 1999-04-23 added thus, hence;
1999-04-22 wenzelm 1999-04-22 switch_theory: Context.pass;
1999-03-19 wenzelm 1999-03-19 common qed and end of proofs;
1999-03-17 wenzelm 1999-03-17 added '_i' versions; add_constdefs; apply_theorems; fixed assume block nest;
1999-03-11 wenzelm 1999-03-11 add_title;
1999-03-09 wenzelm 1999-03-09 begin/end_theory: presentation;
1999-02-08 wenzelm 1999-02-08 Context.fetch, Context.setmp;
1999-02-05 wenzelm 1999-02-05 made MLWorks happy;
1999-02-05 wenzelm 1999-02-05 improved theory, context, update_context;
1999-02-03 wenzelm 1999-02-03 ThyInfo.begin_theory;
1999-01-12 wenzelm 1999-01-12 'same' method, 'immediate' proof;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-11-25 wenzelm 1998-11-25 add_text, add_chapter etc.: dummy;
1998-11-19 wenzelm 1998-11-19 match_bind: 'as' patterns; statements: 'is' patterns;
1998-11-18 wenzelm 1998-11-18 tuned comments;
1998-11-17 wenzelm 1998-11-17 added have_theorems, have_lemmas, have_facts; tuned from_facts; Theory.apply replaced by Library.apply;
1998-11-16 wenzelm 1998-11-16 renamed tac / etac to refine / then_refine;
1998-11-09 wenzelm 1998-11-09 Derived theory operations.