2002-01-12 ago renamed forall_elim_vars_safe to gen_all;
2001-12-14 ago changed Thm.varifyT';
2001-11-29 ago general type of delete_tagged_brl;
2001-11-21 ago use tracing function for trace output;
2001-11-15 ago prove: raise ERROR_MESSAGE;
2001-11-13 ago prove: Envir.beta_norm;
2001-11-11 ago added conjunction_tac;
2001-10-28 ago tuned prove;
2001-10-27 ago tuned prove;
2001-10-27 ago prove: primitive goal interface for internal use;
2001-10-25 ago innermost_params;
2001-10-15 ago qualify some names;
2001-10-14 ago unified rewrite/rewrite_cterm/simplify interface;
2001-10-14 ago tuned full_rewrite;
2001-10-04 ago added full_rewrite_cterm;
2001-01-07 ago tuned norm_hhf(_tac);
2001-01-06 ago added norm_hhf(_tac);
2000-11-10 ago added rewrite_goal_tac;
2000-11-07 ago moved rewriting functions from Drule to MetaSimplifier
2000-10-27 ago added instantiate_tac
2000-08-04 ago added rename_params_tac;
2000-05-25 ago res_inst_tac, etc., no longer print the "dest_state" message when the selected
2000-01-17 ago Thm.instantiate no longer normalizes, but Drule.instantiate does
1999-09-25 ago added fold_rule;
1999-09-06 ago added ftac, eatac, datac, fatac
1999-08-18 ago new primitive rule permute_prems to underlie defer_tac and rotate_prems
1999-07-12 ago removed metacuts_tac;
1999-07-10 ago defer_tac: use try for general exn handling;
1999-03-17 ago qualify Theory.sign_of etc.;
1998-11-26 ago Added filter_prems_tac
1998-11-25 ago replaced prs by writeln;
1998-11-09 ago added metacuts_tac;
1998-08-06 ago added solve_tac;
1998-03-10 ago New simplifier flag for mutual simplification.
1998-03-09 ago adapted to baroque chars;
1998-02-07 ago moved freeze_thaw to drule.ML
1997-12-19 ago adapted to new sort function;
1997-11-21 ago changed Sequence interface (now Seq, in seq.ML);
1997-11-12 ago tuned warning msg;
1997-11-06 ago subgoal_tac displays a warning if the new subgoal has type variables
1997-10-24 ago ProtoPure.thy;
1997-10-24 ago Modified comment.
1997-09-25 ago Generalized and exported biresolution_from_nets_tac to allow the declaration
1997-07-25 ago improved rewrite_thm / rewrite_goals to handle conditional eqns;
1997-07-23 ago tuned apsome;
1997-07-22 ago Removal of the tactical STATE
1997-06-05 ago Tidying of signature. More robust renaming in freeze_thaw.
1997-03-19 ago delete_tagged_brl just ignores non-elimination rules instead of complaining
1997-02-28 ago rule_by_tactic no longer standardizes its result
1997-02-21 ago Replaced "flat" by the Basis Library function List.concat
1997-02-04 ago Gradual switching to Basis Library functions nth, drop, etc.
1996-11-26 ago Eta-expansion of a function definition, for value polymorphism
1996-11-01 ago asm_rewrite_goal_tac now calls SELECT_GOAL.
1996-09-30 ago prune_params_tac no longer rewrites main goal
1996-09-26 ago Generalized freeze to freeze_thaw in order to
1996-09-11 ago renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
1996-09-09 ago added cterm_lift_inst_rule
1996-09-05 ago Added thin_tac to signature; previous change was useless
1996-09-05 ago Declared thin_tac
1996-06-14 ago Added delete function for brls