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.
1996-01-29 clasohm 1996-01-29 inserted tabs again
1996-01-29 clasohm 1996-01-29 removed tabs
1995-07-28 nipkow 1995-07-28 added rotate_tac.
1995-04-28 lcp 1995-04-28 Renamed insert_kbrl to insert_tagged_brl and exported it. Now subgoals_of_brl calls nprems_of, which is faster than length o prems_of.
1995-03-14 nipkow 1995-03-14 Removed an old bug which made some simultaneous instantiations fail if they were given in the "wrong" order. Rewrote sign/infer_types. Fixed some comments.
1995-03-13 nipkow 1995-03-13 Changed treatment of during type inference internally generated type variables. 1. They are renamed to 'a, 'b, 'c etc away from a given set of used names. 2. They are either frozen (turned into TFrees) or left schematic (TVars) depending on a parameter. In goals they are frozen, for instantiations they are left schematic.
1995-03-11 lcp 1995-03-11 Put freeze into the signature TACTIC for export
1995-03-03 clasohm 1995-03-03 added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1994-12-08 lcp 1994-12-08 res_inst_tac: added comments
1994-10-31 lcp 1994-10-31 Pure/tactic/build_netpair: now takes two arguments
1994-06-24 lcp 1994-06-24 Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
1994-02-16 lcp 1994-02-16 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead instantiate changes the indices of V and W. tactic/cut_inst_tac: new
1994-01-18 lcp 1994-01-18 Many other files modified as follows: s|Sign.cterm|cterm|g s|Sign.ctyp|ctyp|g s|Sign.rep_cterm|rep_cterm|g s|Sign.rep_ctyp|rep_ctyp|g s|Sign.pprint_cterm|pprint_cterm|g s|Sign.pprint_ctyp|pprint_ctyp|g s|Sign.string_of_cterm|string_of_cterm|g s|Sign.string_of_ctyp|string_of_ctyp|g s|Sign.term_of|term_of|g s|Sign.typ_of|typ_of|g s|Sign.read_cterm|read_cterm|g s|Sign.read_insts|read_insts|g s|Sign.cfun|cterm_fun|g
1994-01-05 nipkow 1994-01-05 added new parameter to the simplification tactics which indicates if assumptions are to be simplified and/or to be used when simplifying the conclusion. This gets rid of METAHYPS and speeds up simplification of goals with big assumptions.
1993-12-10 lcp 1993-12-10 Pure/tactic/compose_inst_tac: when catching exception THM, prints the message before failing!! This reports the reason for failure in cases like by (res_inst_tac [("P", "?Q(a)")] mp 1); in which ?Q appears in mp with a different type.
1993-10-22 lcp 1993-10-22 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the right sides of the defs
1993-09-16 clasohm 1993-09-16 Initial revision