src/Pure/tactic.ML
2002-10-17 paulson 2002-10-17 fixing the cut_tac method to work when there are no instantiations and the supplied theorems have premises
2002-09-05 paulson 2002-09-05 added checking so that (rename_tac "x y") is rejected, since "x y" is not an identifier
2002-05-07 wenzelm 2002-05-07 use eq_thm_prop instead of slightly inadequate eq_thm;
2002-01-24 wenzelm 2002-01-24 fixed subgoal_tac; fails on non-existent subgoal;
2002-01-17 wenzelm 2002-01-17 renamed norm_hhf to norm_hhf_rule; removed slow rewrite_cterm;
2002-01-16 wenzelm 2002-01-16 tune norm_hhf_tac;
2002-01-12 wenzelm 2002-01-12 renamed forall_elim_vars_safe to gen_all;
2001-12-14 wenzelm 2001-12-14 changed Thm.varifyT';
2001-11-29 wenzelm 2001-11-29 general type of delete_tagged_brl; tuned;
2001-11-21 wenzelm 2001-11-21 use tracing function for trace output;
2001-11-15 wenzelm 2001-11-15 prove: raise ERROR_MESSAGE;
2001-11-13 wenzelm 2001-11-13 prove: Envir.beta_norm;
2001-11-11 wenzelm 2001-11-11 added conjunction_tac;
2001-10-28 wenzelm 2001-10-28 tuned prove;
2001-10-27 wenzelm 2001-10-27 tuned prove; added prove_standard;
2001-10-27 wenzelm 2001-10-27 prove: primitive goal interface for internal use;
2001-10-25 wenzelm 2001-10-25 innermost_params;
2001-10-15 wenzelm 2001-10-15 qualify some names;
2001-10-14 wenzelm 2001-10-14 unified rewrite/rewrite_cterm/simplify interface;
2001-10-14 wenzelm 2001-10-14 tuned full_rewrite;
2001-10-04 wenzelm 2001-10-04 added full_rewrite_cterm;
2001-01-07 wenzelm 2001-01-07 tuned norm_hhf(_tac);
2001-01-06 wenzelm 2001-01-06 added norm_hhf(_tac);
2000-11-10 wenzelm 2000-11-10 added rewrite_goal_tac;
2000-11-07 berghofe 2000-11-07 moved rewriting functions from Drule to MetaSimplifier
2000-10-27 oheimb 2000-10-27 added instantiate_tac
2000-08-04 wenzelm 2000-08-04 added rename_params_tac;
2000-05-25 paulson 2000-05-25 res_inst_tac, etc., no longer print the "dest_state" message when the selected subgoal does not exist
2000-01-17 paulson 2000-01-17 Thm.instantiate no longer normalizes, but Drule.instantiate does
1999-09-25 wenzelm 1999-09-25 added fold_rule;
1999-09-06 oheimb 1999-09-06 added ftac, eatac, datac, fatac
1999-08-18 paulson 1999-08-18 new primitive rule permute_prems to underlie defer_tac and rotate_prems
1999-07-12 wenzelm 1999-07-12 removed metacuts_tac;
1999-07-10 wenzelm 1999-07-10 defer_tac: use try for general exn handling;
1999-03-17 wenzelm 1999-03-17 qualify Theory.sign_of etc.;
1998-11-26 nipkow 1998-11-26 Added filter_prems_tac
1998-11-25 wenzelm 1998-11-25 replaced prs by writeln;
1998-11-09 wenzelm 1998-11-09 added metacuts_tac;
1998-08-06 wenzelm 1998-08-06 added solve_tac;
1998-03-10 nipkow 1998-03-10 New simplifier flag for mutual simplification.
1998-03-09 wenzelm 1998-03-09 adapted to baroque chars;
1998-02-07 paulson 1998-02-07 moved freeze_thaw to drule.ML
1997-12-19 wenzelm 1997-12-19 adapted to new sort function;
1997-11-21 wenzelm 1997-11-21 changed Sequence interface (now Seq, in seq.ML);
1997-11-12 wenzelm 1997-11-12 tuned warning msg;
1997-11-06 paulson 1997-11-06 subgoal_tac displays a warning if the new subgoal has type variables
1997-10-24 wenzelm 1997-10-24 ProtoPure.thy;
1997-10-24 nipkow 1997-10-24 Modified comment.
1997-09-25 paulson 1997-09-25 Generalized and exported biresolution_from_nets_tac to allow the declaration of Clarify_tac
1997-07-25 wenzelm 1997-07-25 improved rewrite_thm / rewrite_goals to handle conditional eqns;
1997-07-23 wenzelm 1997-07-23 tuned apsome;
1997-07-22 paulson 1997-07-22 Removal of the tactical STATE
1997-06-05 paulson 1997-06-05 Tidying of signature. More robust renaming in freeze_thaw. New tactic distinct_subgoals_tac
1997-03-19 paulson 1997-03-19 delete_tagged_brl just ignores non-elimination rules instead of complaining
1997-02-28 paulson 1997-02-28 rule_by_tactic no longer standardizes its result
1997-02-21 paulson 1997-02-21 Replaced "flat" by the Basis Library function List.concat
1997-02-04 paulson 1997-02-04 Gradual switching to Basis Library functions nth, drop, etc.
1996-11-26 paulson 1996-11-26 Eta-expansion of a function definition, for value polymorphism
1996-11-01 paulson 1996-11-01 asm_rewrite_goal_tac now calls SELECT_GOAL. Replaced min by Int.min
1996-09-30 paulson 1996-09-30 prune_params_tac no longer rewrites main goal