2001-11-26 ago added remdups_rl;
2001-11-24 ago gen_merge_lists';
2001-11-16 ago local_standard: plain strip_shyps instead of strip_shyps_warning;
2001-11-11 ago added conj_elim_precise, conj_intr_thm;
2001-11-09 ago Theorems symmetric, reflexive and transitive are now stored with "open"
2001-11-07 ago tuned impose_hyps;
2001-11-05 ago export add_tvarsT, add_tvars, add_vars, add_frees (would actually
2001-10-31 ago added local_standard;
2001-10-31 ago norm_hhf_eq is now stored using open_store_standard_thm.
2001-10-28 ago rules for meta-level conjunction;
2001-10-27 ago added impose_hyps;
2001-10-16 ago added implies_intr_goals;
2001-10-13 ago generic theorem kinds ("theorem", "lemma" etc.);
2001-08-31 ago Some basic rules are now stored with "open" derivations, to facilitate
2001-02-20 ago added rearrange_prems
2001-02-14 ago imp_cong2 -> imp_cong
2001-01-07 ago removed outdated comment;
2001-01-03 ago Thm: dest_comb, dest_abs, capply, cabs no longer global;
2000-12-13 ago eliminated GOAL syntax;
2000-11-23 ago standard: close_derivation;
2000-11-10 ago store_standard_thm "norm_hhf_eq";
2000-11-07 ago - new theorems imp_cong and swap_prems_eq
2000-11-06 ago Sign.typ_instance;
2000-09-05 ago improved add_rules;
2000-09-04 ago added add_rules, del_rules;
2000-08-08 ago added forall_elim_vars_safe, norm_hhf_eq;
2000-08-07 ago more cterm operations: mk_implies, list_implies
2000-07-30 ago Logic.goal_const;
2000-07-27 ago export has_internal;
2000-07-24 ago Drule.merge_rules;
2000-07-12 ago infix 'OF' is a version of 'MRS' with more appropriate argument order;
2000-03-30 ago added tvars_intr_list;
2000-03-22 ago new meta-rule "inst", a shorthand for read_instantiate_sg
2000-03-17 ago untag: remove all tags of given name;
2000-03-10 ago Type.unify and Type.typ_match now use Vartab instead of association lists.
2000-03-08 ago added (un)tag_rule;
2000-03-02 ago added freeze_all;
2000-01-17 ago Thm.instantiate no longer normalizes, but Drule.instantiate does
2000-01-05 ago TypeInfer.logicT;
1999-10-21 ago forall_elim_var(s) moved to pure_thy.ML;
1999-09-29 ago strip_shyps_warning;
1999-09-04 ago handle Bind!!
1999-09-01 ago PureThy.smart_store_thms;
1999-08-27 ago thm "_" = asm_rl;
1999-08-18 ago new primitive rule permute_prems to underlie defer_tac and rotate_prems
1999-07-13 ago added mk_cgoal, assume_goal;
1999-07-09 ago added compose_single;
1999-07-08 ago improved error msgs of cterm_instantiate;
1999-04-16 ago added incr_indexes, incr_indexes_wrt;
1999-03-17 ago qualify Theory.sign_of etc.;
1999-01-12 ago added rule_attribute: ('a -> thm -> thm) -> 'a attribute;
1998-11-17 ago export vars_of and friends;
1998-10-20 ago added unvarify(T);
1998-08-13 ago Rule mk_triv_goal for making instances of triv_goal
1998-06-25 ago added rewrite_cterm;
1998-04-04 ago added triv_goal, rev_triv_goal (for Isar);
1998-03-10 ago New simplifier flag for mutual simplification.
1998-03-09 ago Syntax.indexname;
1998-03-04 ago Reorganized simplifier. May now reorient rules.
1998-02-07 ago Tidying; rotate_prems; moved freeze_thaw from tactic.ML