src/Pure/tactic.ML
Thu, 25 Sep 1997 12:09:41 +0200 paulson Generalized and exported biresolution_from_nets_tac to allow the declaration
Fri, 25 Jul 1997 11:47:09 +0200 wenzelm improved rewrite_thm / rewrite_goals to handle conditional eqns;
Wed, 23 Jul 1997 10:22:30 +0200 wenzelm tuned apsome;
Tue, 22 Jul 1997 11:14:18 +0200 paulson Removal of the tactical STATE
Thu, 05 Jun 1997 13:52:43 +0200 paulson Tidying of signature. More robust renaming in freeze_thaw.
Wed, 19 Mar 1997 10:24:39 +0100 paulson delete_tagged_brl just ignores non-elimination rules instead of complaining
Fri, 28 Feb 1997 15:46:41 +0100 paulson rule_by_tactic no longer standardizes its result
Fri, 21 Feb 1997 15:31:47 +0100 paulson Replaced "flat" by the Basis Library function List.concat
Tue, 04 Feb 1997 10:33:58 +0100 paulson Gradual switching to Basis Library functions nth, drop, etc.
Tue, 26 Nov 1996 16:18:42 +0100 paulson Eta-expansion of a function definition, for value polymorphism
Fri, 01 Nov 1996 15:30:49 +0100 paulson asm_rewrite_goal_tac now calls SELECT_GOAL.
Mon, 30 Sep 1996 10:59:47 +0200 paulson prune_params_tac no longer rewrites main goal
Thu, 26 Sep 1996 11:10:46 +0200 paulson Generalized freeze to freeze_thaw in order to
Wed, 11 Sep 1996 18:00:53 +0200 nipkow renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
Mon, 09 Sep 1996 18:53:41 +0200 nipkow added cterm_lift_inst_rule
Thu, 05 Sep 1996 18:29:43 +0200 paulson Added thin_tac to signature; previous change was useless
Thu, 05 Sep 1996 10:29:52 +0200 paulson Declared thin_tac
Fri, 14 Jun 1996 12:27:11 +0200 paulson Added delete function for brls
Fri, 16 Feb 1996 12:34:18 +0100 paulson Elimination of fully-functorial style.
Mon, 29 Jan 1996 14:16:13 +0100 clasohm inserted tabs again
Mon, 29 Jan 1996 13:56:41 +0100 clasohm removed tabs
Fri, 28 Jul 1995 17:24:53 +0200 nipkow added rotate_tac.
Fri, 28 Apr 1995 11:52:43 +0200 lcp Renamed insert_kbrl to insert_tagged_brl and exported it. Now
Tue, 14 Mar 1995 10:40:04 +0100 nipkow Removed an old bug which made some simultaneous instantiations fail if they
Mon, 13 Mar 1995 09:38:10 +0100 nipkow Changed treatment of during type inference internally generated type
Sat, 11 Mar 1995 11:58:21 +0100 lcp Put freeze into the signature TACTIC for export
Fri, 03 Mar 1995 11:48:05 +0100 clasohm added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
Thu, 08 Dec 1994 11:26:25 +0100 lcp res_inst_tac: added comments
Mon, 31 Oct 1994 18:01:02 +0100 lcp Pure/tactic/build_netpair: now takes two arguments
Fri, 24 Jun 1994 10:45:02 +0200 lcp Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
Wed, 16 Feb 1994 13:56:20 +0100 lcp tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
Tue, 18 Jan 1994 15:57:40 +0100 lcp Many other files modified as follows:
Wed, 05 Jan 1994 19:33:56 +0100 nipkow added new parameter to the simplification tactics which indicates if
Fri, 10 Dec 1993 10:36:39 +0100 lcp Pure/tactic/compose_inst_tac: when catching exception THM, prints the
Fri, 22 Oct 1993 11:25:15 +0100 lcp tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip