src/Pure/tactic.ML
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;
Wed, 12 Jul 2006 21:19:19 +0200 wenzelm exported make_elim_preserve;
Mon, 19 Jun 2006 20:21:30 +0200 wenzelm eliminated freeze/varify in favour of Variable.import/export/trade;
Mon, 29 May 2006 13:15:53 +0200 paulson fixing a variable-clash bug in rule_by_tactic
Tue, 02 May 2006 14:27:49 +0200 paulson tidied and harmonized "params_of_state"
Thu, 27 Apr 2006 15:06:35 +0200 wenzelm tuned basic list operators (flat, maps, map_filter);
Wed, 26 Apr 2006 22:38:05 +0200 wenzelm tuned;
Thu, 13 Apr 2006 12:01:01 +0200 wenzelm use conjunction stuff from conjunction.ML;
Sat, 04 Mar 2006 21:10:09 +0100 wenzelm tuned conj_curry;
Wed, 22 Feb 2006 22:18:39 +0100 wenzelm simplified Pure conjunction, based on actual const;
Wed, 15 Feb 2006 21:35:06 +0100 wenzelm sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
Wed, 08 Feb 2006 14:39:00 +0100 haftmann introduced gen_distinct in place of distinct
Fri, 23 Dec 2005 15:16:49 +0100 wenzelm CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
Thu, 22 Dec 2005 00:29:01 +0100 wenzelm conjunction_tac: single goal;
Sat, 19 Nov 2005 14:21:06 +0100 wenzelm added CONJUNCTS: treat conjunction as separate sub-goals;
Thu, 10 Nov 2005 20:57:11 +0100 wenzelm renamed Thm.cgoal_of to Thm.cprem_of;
Fri, 28 Oct 2005 22:28:03 +0200 wenzelm accomodate simplified Thm.lift_rule;
Fri, 21 Oct 2005 18:14:48 +0200 wenzelm moved norm_hhf_rule, prove etc. to goal.ML;
Tue, 18 Oct 2005 17:59:25 +0200 wenzelm Simplifier.theory_context;
less more (0) -100 -60 tip