src/Pure/tactic.ML
Fri, 10 Sep 2021 14:59:19 +0200 wenzelm clarified signature: more scalable operations;
Mon, 01 Oct 2018 16:41:36 +0200 wenzelm more direct implementation of distinct_subgoals_tac -- potentially more efficient;
Tue, 28 Aug 2018 10:58:43 +0200 wenzelm clarified signature: do not expose internal operation;
Sun, 25 Feb 2018 15:44:46 +0100 wenzelm eliminated ASCII syntax from Pure bootstrap;
Sun, 26 Jul 2015 22:26:11 +0200 wenzelm eliminated atac, rtac, etac, dtac, ftac;
Fri, 24 Jul 2015 22:20:22 +0200 wenzelm proper context;
Fri, 24 Jul 2015 22:19:36 +0200 wenzelm unused;
Fri, 24 Jul 2015 22:16:39 +0200 wenzelm proper context;
Thu, 19 Mar 2015 11:54:20 +0100 wenzelm tuned comments;
Wed, 04 Mar 2015 20:47:29 +0100 wenzelm tuned;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Sat, 20 Dec 2014 22:23:37 +0100 wenzelm proper context for "net" tactics;
Mon, 10 Nov 2014 21:49:48 +0100 wenzelm proper context for assume_tac (atac remains as fall-back without context);
Sun, 09 Nov 2014 17:04:14 +0100 wenzelm proper context for match_tac etc.;
Sun, 09 Nov 2014 14:08:00 +0100 wenzelm proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
Sat, 08 Nov 2014 21:31:51 +0100 wenzelm optional proof context for unify operations, for the sake of proper local options;
Thu, 30 Oct 2014 16:20:46 +0100 wenzelm eliminated aliases;
Wed, 29 May 2013 18:25:11 +0200 wenzelm tuned signature -- more explicit flags for low-level Thm.bicompose;
Mon, 20 May 2013 17:14:39 +0200 wenzelm more precise treatment of theory vs. Proof.context;
Wed, 03 Apr 2013 16:45:14 +0200 wenzelm tuned -- Drule.comp_no_flatten includes Drule.incr_indexes already (NB: result should be deterministic by construction);
Mon, 26 Nov 2012 21:46:04 +0100 wenzelm tuned signature;
Sun, 11 Nov 2012 20:31:46 +0100 wenzelm tuned;
Tue, 16 Oct 2012 17:47:23 +0200 wenzelm clarified defer/prefer: more specific errors;
Mon, 27 Feb 2012 15:00:19 +0100 wenzelm simplified cut_tac (cf. d549b5b0f344);
Tue, 14 Feb 2012 21:31:26 +0100 wenzelm eliminated odd/obsolete innermost_params (cf. a77ad6c86564, 3458b0e955ac);
Tue, 14 Feb 2012 17:11:33 +0100 wenzelm eliminated obsolete aliases;
Fri, 08 Apr 2011 16:34:14 +0200 wenzelm discontinued special treatment of structure Lexicon;
Sat, 15 May 2010 21:41:32 +0200 wenzelm less pervasive names from structure Thm;
Fri, 30 Apr 2010 18:06:29 +0200 wenzelm proper context for rule_by_tactic;
Mon, 26 Apr 2010 20:30:50 +0200 wenzelm eliminanated some unreferenced identifiers;
Sat, 06 Mar 2010 14:35:06 +0100 wenzelm removed unused term_lift_inst_rule (superceded by Subgoal.FOCUS etc.);
Wed, 25 Nov 2009 09:13:46 +0100 haftmann normalized uncurry take/drop
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Sat, 17 Oct 2009 17:18:59 +0200 wenzelm less pervasive names;
Mon, 06 Jul 2009 21:24:30 +0200 wenzelm structure Thm: less pervasive names;
Wed, 24 Jun 2009 21:28:02 +0200 wenzelm renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
Sun, 24 May 2009 15:02:23 +0200 haftmann tuned whitespace
Tue, 17 Mar 2009 14:09:20 +0100 wenzelm renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
Wed, 31 Dec 2008 19:54:03 +0100 wenzelm qualified Term.rename_wrt_term;
Mon, 16 Jun 2008 22:13:50 +0200 wenzelm removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML);
Sat, 14 Jun 2008 23:19:57 +0200 wenzelm qualified old res_inst_tac variants;
Wed, 11 Jun 2008 18:04:02 +0200 wenzelm Drule.read_instantiate;
Sat, 12 Apr 2008 17:00:35 +0200 wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
Thu, 27 Mar 2008 14:41:09 +0100 wenzelm eliminated theory ProtoPure;
Mon, 21 Jan 2008 14:18:49 +0100 berghofe Removed Logic.auto_rename.
Mon, 13 Aug 2007 18:10:22 +0200 wenzelm Lexicon.read_indexname/nat/variable;
Tue, 03 Jul 2007 17:17:13 +0200 wenzelm removed obsolete eta_long_tac;
Mon, 25 Jun 2007 00:36:41 +0200 wenzelm added eta_long_tac;
Sun, 03 Jun 2007 23:16:51 +0200 wenzelm cleaned up signature;
Thu, 31 May 2007 23:47:36 +0200 wenzelm simplified/unified list fold;
Wed, 04 Apr 2007 00:11:14 +0200 wenzelm added scanwords from library.ML (for obsolete rename_tac);
Tue, 03 Apr 2007 19:24:13 +0200 wenzelm renamed Variable.import to import_thms (avoid clash with Alice keywords);
Mon, 02 Apr 2007 11:30:44 +0200 paulson now exports distinct_subgoal_tac (needed by MetisAPI)
Mon, 26 Feb 2007 23:18:24 +0100 wenzelm moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
Thu, 07 Dec 2006 23:16:55 +0100 wenzelm reorganized structure Tactic vs. MetaSimplifier;
Thu, 07 Dec 2006 00:42:04 +0100 wenzelm reorganized structure Goal vs. Tactic;
Wed, 02 Aug 2006 22:26:56 +0200 wenzelm renamed Syntax.indexname to Syntax.read_indexname;
Thu, 27 Jul 2006 13:43:10 +0200 wenzelm removed obsolete is_fact (cf. Thm.no_prems);
Wed, 26 Jul 2006 19:37:41 +0200 wenzelm Variable.import(T): result includes fixed types/terms;
less more (0) -100 -60 tip