| Thu, 17 May 2007 22:37:34 +0200 |
krauss |
added pointer to new Unification theory
|
file |
diff |
annotate
|
| Mon, 05 Jun 2006 14:22:58 +0200 |
krauss |
Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
|
file |
diff |
annotate
|
| Fri, 12 May 2006 11:19:41 +0200 |
nipkow |
added lemma in_measure
|
file |
diff |
annotate
|
| Fri, 01 Apr 2005 21:04:00 +0200 |
paulson |
x-symbols and other tidying
|
file |
diff |
annotate
|
| Tue, 29 Mar 2005 12:30:48 +0200 |
paulson |
converted HOL-Subst to tactic scripts
|
file |
diff |
annotate
|
| Thu, 06 Dec 2001 00:46:24 +0100 |
wenzelm |
use Main;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2000 15:01:50 +0200 |
nipkow |
Times -> <*>
|
file |
diff |
annotate
|
| Thu, 22 Apr 1999 13:04:23 +0200 |
wenzelm |
recdef requires theory Recdef;
|
file |
diff |
annotate
|
| Thu, 22 May 1997 15:10:37 +0200 |
paulson |
Now uses type option instead of Fail/Subst
|
file |
diff |
annotate
|
| Wed, 21 May 1997 10:53:38 +0200 |
paulson |
Removed rprod from the WF relation
|
file |
diff |
annotate
|
| Thu, 15 May 1997 12:40:01 +0200 |
paulson |
New version, modified by Konrad Slind and LCP for TFL
|
file |
diff |
annotate
|