src/Provers/hypsubst.ML
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Thu, 08 Nov 2012 19:55:35 +0100 bulwahn hyp_subst_tac allows to pass an optional simpset to the internal simplifier call to avoid renamed bound variable warnings in the simplifier call
Tue, 19 Jun 2012 11:18:09 +0200 Rafal Kolanski Updated comment to reflect current state.
Sat, 14 Jan 2012 21:16:15 +0100 wenzelm discontinued old-style Term.list_abs in favour of plain Term.abs;
Mon, 28 Nov 2011 17:05:41 +0100 wenzelm avoid stepping outside of context -- plain zero_var_indexes should be sufficient;
Thu, 24 Nov 2011 21:01:06 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Mon, 08 Aug 2011 17:23:15 +0200 wenzelm misc tuning -- eliminated old-fashioned rep_thm;
Thu, 09 Jun 2011 23:12:02 +0200 wenzelm renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
Sat, 14 May 2011 11:42:43 +0200 wenzelm modernized functor names;
Sat, 16 Apr 2011 20:26:59 +0200 wenzelm more direct Thm.cprem_of (with exception THM instead of Subscript);
Sat, 16 Apr 2011 18:11:20 +0200 wenzelm eliminated old List.nth;
Thu, 24 Mar 2011 16:47:24 +0100 wenzelm more direct loose_bvar1;
Wed, 29 Sep 2010 11:02:24 +0200 krauss backed out my old attempt at single_hyp_subst_tac (67cd6ed76446)
Fri, 10 Sep 2010 23:56:35 +0200 krauss use eta-contracted version for occurrence check (avoids possible non-termination)
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
Thu, 29 Apr 2010 22:56:32 +0200 wenzelm proper context for mksimps etc. -- via simpset of the running Simplifier;
Sat, 13 Mar 2010 16:44:12 +0100 wenzelm removed old CVS Ids;
Fri, 19 Feb 2010 16:11:45 +0100 wenzelm renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Sat, 17 Oct 2009 00:52:37 +0200 wenzelm explicitly qualify Drule.standard;
Fri, 13 Mar 2009 23:50:05 +0100 wenzelm simplified method setup;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Mon, 04 Aug 2008 22:55:00 +0200 wenzelm meta_subst: xsymbols make it work with clean Pure;
Mon, 14 Jul 2008 17:47:18 +0200 krauss single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
Sat, 24 May 2008 23:52:35 +0200 wenzelm inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
Wed, 07 May 2008 10:59:48 +0200 berghofe Added function for computing instantiation for the subst rule, which is used
Sun, 22 Jul 2007 21:20:53 +0200 wenzelm blast_hyp_subst_tac: plain bool argument;
Wed, 29 Nov 2006 15:44:51 +0100 wenzelm simplified method setup;
Tue, 07 Nov 2006 19:39:46 +0100 wenzelm avoid handling of arbitrary exceptions;
Tue, 07 Nov 2006 14:30:03 +0100 wenzelm simplified dest_eq;
Wed, 11 Oct 2006 14:51:25 +0200 haftmann slight type signature changes
Tue, 10 Oct 2006 10:36:14 +0200 haftmann fixed intendation
Tue, 11 Jul 2006 12:16:59 +0200 wenzelm Name.is_bound;
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Tue, 18 Oct 2005 17:59:29 +0200 wenzelm functor: no Simplifier argument;
Mon, 01 Aug 2005 19:20:33 +0200 wenzelm Term.is_bound;
Thu, 07 Apr 2005 09:26:10 +0200 wenzelm improved comments;
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Tue, 01 Feb 2005 18:01:57 +0100 paulson the new subst tactic, by Lucas Dixon
Thu, 16 Dec 2004 12:44:32 +0100 paulson fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
Mon, 30 Sep 2002 16:34:56 +0200 berghofe - eliminated thin_leading_eqs_tac
Wed, 05 Dec 2001 03:13:21 +0100 wenzelm 'symmetric' attribute moved to Pure/calculation.ML;
Wed, 21 Nov 2001 00:36:51 +0100 wenzelm use tracing function for trace output;
Sun, 07 Jan 2001 21:41:56 +0100 wenzelm CHANGED_PROP;
Thu, 07 Sep 2000 20:51:07 +0200 wenzelm tuned msg;
Mon, 28 Aug 2000 20:31:00 +0200 wenzelm Method.SIMPLE_METHOD';
Thu, 17 Aug 2000 10:39:12 +0200 wenzelm added 'symmetric' attribute;
Mon, 14 Aug 2000 14:53:47 +0200 wenzelm added hypsubst;
Fri, 04 Aug 2000 22:58:23 +0200 wenzelm added rev_eq_reflection;
Tue, 23 Dec 1997 11:39:03 +0100 paulson Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
Wed, 26 Nov 1997 16:49:07 +0100 paulson updated comment
Wed, 12 Nov 1997 18:58:50 +0100 oheimb added thin_refl to hyp_subst_tac
Thu, 06 Nov 1997 10:29:37 +0100 paulson hyp_subst_tac checks if the equality has type variables and uses a suitable
Tue, 22 Jul 1997 11:12:55 +0200 paulson Removal of the tactical STATE
Fri, 07 Mar 1997 10:22:54 +0100 paulson Prevent permutation of assumptions in hyp_subst_tac
Wed, 05 Mar 1997 10:01:57 +0100 paulson Now uses rotate_tac and eta_contract_atom for greater speed
Tue, 12 Nov 1996 11:36:44 +0100 paulson Removed a call to polymorphic mem
Fri, 01 Nov 1996 15:15:39 +0100 paulson Replaced min by Int.min
Thu, 06 Apr 1995 11:59:34 +0200 lcp Recoded with help from Toby to use rewriting instead of the
Fri, 11 Nov 1994 10:42:55 +0100 lcp Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
less more (0) -60 tip