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;
less more (0) -100 -50 -30 tip