src/Pure/tactic.ML
Tue, 20 Sep 2005 08:21:49 +0200 haftmann slight adaptions to library changes
Tue, 06 Sep 2005 08:30:43 +0200 haftmann introduced some new-style AList operations
Wed, 31 Aug 2005 15:46:40 +0200 wenzelm refer to theory instead of low-level tsig;
Thu, 28 Jul 2005 15:19:59 +0200 wenzelm norm_hhf_rule: Thm.adjust_maxidx_thm before Drule.gen_all;
Tue, 19 Jul 2005 17:21:47 +0200 wenzelm Logic.incr_tvar;
Wed, 13 Jul 2005 16:07:30 +0200 wenzelm export eq_brl;
Fri, 01 Jul 2005 22:34:50 +0200 wenzelm cterm_aconv: avoid rep_cterm;
Fri, 17 Jun 2005 18:33:08 +0200 wenzelm accomodate identification of type Sign.sg and theory;
Wed, 08 Jun 2005 16:11:09 +0200 ballarin Fixed "axiom" generation for mixed locales with and without predicates.
Tue, 17 May 2005 17:01:35 +0200 paulson added comment
Thu, 28 Apr 2005 21:35:25 +0200 wenzelm added smart_conjunction_tac, prove_multi, prove_multi_standard;
Thu, 21 Apr 2005 19:12:03 +0200 berghofe - Eliminated nodup_vars check.
Mon, 11 Apr 2005 12:34:34 +0200 ballarin First release of interpretation commands.
Thu, 07 Apr 2005 09:27:50 +0200 wenzelm Drule.add_used;
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Mon, 24 Jan 2005 18:18:28 +0100 berghofe Added variant of eres_inst_tac that operates on indexnames instead of strings.
Mon, 24 Jan 2005 12:40:52 +0100 paulson some rationalizing of res_inst_tac
Tue, 18 Jan 2005 14:34:24 +0100 berghofe Added variants of instantiation functions that operate on pairs of type
Thu, 08 Jul 2004 19:33:05 +0200 wenzelm got rid of obsolete meta_simpset;
Wed, 30 Jun 2004 00:42:59 +0200 skalberg Made simplification procedures simpset-aware.
Fri, 25 Jun 2004 14:30:55 +0200 skalberg Merging the meta-simplifier with the Provers-simplifier. Next step:
Mon, 26 Apr 2004 14:54:45 +0200 wenzelm use Syntax.is_identifier;
Sat, 26 Apr 2003 12:38:17 +0200 paulson catches exception DELETE
Thu, 17 Oct 2002 10:52:59 +0200 paulson fixing the cut_tac method to work when there are no instantiations and the
Thu, 05 Sep 2002 14:03:03 +0200 paulson added checking so that (rename_tac "x y") is rejected, since
Tue, 07 May 2002 14:26:32 +0200 wenzelm use eq_thm_prop instead of slightly inadequate eq_thm;
Thu, 24 Jan 2002 22:42:14 +0100 wenzelm fixed subgoal_tac; fails on non-existent subgoal;
Thu, 17 Jan 2002 21:03:29 +0100 wenzelm renamed norm_hhf to norm_hhf_rule;
Wed, 16 Jan 2002 22:24:37 +0100 wenzelm tune norm_hhf_tac;
Sat, 12 Jan 2002 16:37:58 +0100 wenzelm renamed forall_elim_vars_safe to gen_all;
Fri, 14 Dec 2001 11:52:54 +0100 wenzelm changed Thm.varifyT';
Thu, 29 Nov 2001 00:44:34 +0100 wenzelm general type of delete_tagged_brl;
Wed, 21 Nov 2001 00:36:51 +0100 wenzelm use tracing function for trace output;
Thu, 15 Nov 2001 18:36:07 +0100 wenzelm prove: raise ERROR_MESSAGE;
Tue, 13 Nov 2001 17:51:03 +0100 wenzelm prove: Envir.beta_norm;
Sun, 11 Nov 2001 21:31:52 +0100 wenzelm added conjunction_tac;
Sun, 28 Oct 2001 19:44:26 +0100 wenzelm tuned prove;
Sat, 27 Oct 2001 23:19:04 +0200 wenzelm tuned prove;
Sat, 27 Oct 2001 00:07:19 +0200 wenzelm prove: primitive goal interface for internal use;
Thu, 25 Oct 2001 02:12:10 +0200 wenzelm innermost_params;
Mon, 15 Oct 2001 20:31:52 +0200 wenzelm qualify some names;
Sun, 14 Oct 2001 22:05:46 +0200 wenzelm unified rewrite/rewrite_cterm/simplify interface;
Sun, 14 Oct 2001 20:08:42 +0200 wenzelm tuned full_rewrite;
Thu, 04 Oct 2001 15:21:17 +0200 wenzelm added full_rewrite_cterm;
Sun, 07 Jan 2001 21:36:11 +0100 wenzelm tuned norm_hhf(_tac);
Sat, 06 Jan 2001 21:27:12 +0100 wenzelm added norm_hhf(_tac);
Fri, 10 Nov 2000 19:12:30 +0100 wenzelm added rewrite_goal_tac;
Tue, 07 Nov 2000 17:50:21 +0100 berghofe moved rewriting functions from Drule to MetaSimplifier
Fri, 27 Oct 2000 15:53:47 +0200 oheimb added instantiate_tac
Fri, 04 Aug 2000 22:59:08 +0200 wenzelm added rename_params_tac;
Thu, 25 May 2000 15:22:19 +0200 paulson res_inst_tac, etc., no longer print the "dest_state" message when the selected
Mon, 17 Jan 2000 14:10:32 +0100 paulson Thm.instantiate no longer normalizes, but Drule.instantiate does
Sat, 25 Sep 1999 13:05:38 +0200 wenzelm added fold_rule;
Mon, 06 Sep 1999 18:18:09 +0200 oheimb added ftac, eatac, datac, fatac
Wed, 18 Aug 1999 10:54:44 +0200 paulson new primitive rule permute_prems to underlie defer_tac and rotate_prems
Mon, 12 Jul 1999 22:25:19 +0200 wenzelm removed metacuts_tac;
Sat, 10 Jul 1999 21:41:57 +0200 wenzelm defer_tac: use try for general exn handling;
Wed, 17 Mar 1999 16:33:00 +0100 wenzelm qualify Theory.sign_of etc.;
less more (0) -100 -60 tip