| Wed, 29 Sep 2010 11:02:24 +0200 |
krauss |
backed out my old attempt at single_hyp_subst_tac (67cd6ed76446)
|
file |
diff |
annotate
|
| Fri, 10 Sep 2010 23:56:35 +0200 |
krauss |
use eta-contracted version for occurrence check (avoids possible non-termination)
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 22:56:32 +0200 |
wenzelm |
proper context for mksimps etc. -- via simpset of the running Simplifier;
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 16:44:12 +0100 |
wenzelm |
removed old CVS Ids;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 00:52:37 +0200 |
wenzelm |
explicitly qualify Drule.standard;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 23:50:05 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Mon, 04 Aug 2008 22:55:00 +0200 |
wenzelm |
meta_subst: xsymbols make it work with clean Pure;
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 17:47:18 +0200 |
krauss |
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:59:48 +0200 |
berghofe |
Added function for computing instantiation for the subst rule, which is used
|
file |
diff |
annotate
|
| Sun, 22 Jul 2007 21:20:53 +0200 |
wenzelm |
blast_hyp_subst_tac: plain bool argument;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:44:51 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 19:39:46 +0100 |
wenzelm |
avoid handling of arbitrary exceptions;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 14:30:03 +0100 |
wenzelm |
simplified dest_eq;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 14:51:25 +0200 |
haftmann |
slight type signature changes
|
file |
diff |
annotate
|
| Tue, 10 Oct 2006 10:36:14 +0200 |
haftmann |
fixed intendation
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:16:59 +0200 |
wenzelm |
Name.is_bound;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Tue, 18 Oct 2005 17:59:29 +0200 |
wenzelm |
functor: no Simplifier argument;
|
file |
diff |
annotate
|
| Mon, 01 Aug 2005 19:20:33 +0200 |
wenzelm |
Term.is_bound;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2005 09:26:10 +0200 |
wenzelm |
improved comments;
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
| Thu, 16 Dec 2004 12:44:32 +0100 |
paulson |
fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 16:34:56 +0200 |
berghofe |
- eliminated thin_leading_eqs_tac
|
file |
diff |
annotate
|
| Wed, 05 Dec 2001 03:13:21 +0100 |
wenzelm |
'symmetric' attribute moved to Pure/calculation.ML;
|
file |
diff |
annotate
|