| 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
|
| Wed, 21 Nov 2001 00:36:51 +0100 |
wenzelm |
use tracing function for trace output;
|
file |
diff |
annotate
|
| Sun, 07 Jan 2001 21:41:56 +0100 |
wenzelm |
CHANGED_PROP;
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 20:51:07 +0200 |
wenzelm |
tuned msg;
|
file |
diff |
annotate
|
| Mon, 28 Aug 2000 20:31:00 +0200 |
wenzelm |
Method.SIMPLE_METHOD';
|
file |
diff |
annotate
|
| Thu, 17 Aug 2000 10:39:12 +0200 |
wenzelm |
added 'symmetric' attribute;
|
file |
diff |
annotate
|
| Mon, 14 Aug 2000 14:53:47 +0200 |
wenzelm |
added hypsubst;
|
file |
diff |
annotate
|
| Fri, 04 Aug 2000 22:58:23 +0200 |
wenzelm |
added rev_eq_reflection;
|
file |
diff |
annotate
|