src/Pure/tactic.ML
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
1996-09-26 paulson 1996-09-26 Generalized freeze to freeze_thaw in order to implement defer_tac
1996-09-11 nipkow 1996-09-11 renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take uncertified things, because they need to be recertified anyway.
1996-09-09 nipkow 1996-09-09 added cterm_lift_inst_rule
1996-09-05 paulson 1996-09-05 Added thin_tac to signature; previous change was useless
1996-09-05 paulson 1996-09-05 Declared thin_tac
1996-06-14 paulson 1996-06-14 Added delete function for brls
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.