| Sat, 30 Jan 2010 17:03:46 +0100 |
berghofe |
Adapted to changes in cases method.
|
file |
diff |
annotate
|
| Fri, 18 Sep 2009 09:35:23 +0200 |
haftmann |
simplified proof
|
file |
diff |
annotate
|
| Mon, 27 Jul 2009 21:47:41 +0200 |
krauss |
"more standard" argument order of relation composition (op O)
|
file |
diff |
annotate
|
| Thu, 28 Feb 2008 15:55:33 +0100 |
wenzelm |
Transitive_Closure: induct and cases rules now declare proper case_names;
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 23:05:24 +0100 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Sun, 12 Aug 2007 18:53:03 +0200 |
wenzelm |
added type constraints to resolve syntax ambiguities;
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:23:24 +0200 |
berghofe |
- Renamed inductive2 to inductive
|
file |
diff |
annotate
|
| Fri, 09 Mar 2007 08:45:50 +0100 |
haftmann |
stepping towards uniform lattice theory development in HOL
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:45:03 +0100 |
berghofe |
- Adapted to new inductive definition package
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
file |
diff |
annotate
|
| Mon, 11 Sep 2006 21:35:19 +0200 |
wenzelm |
induct method: renamed 'fixing' to 'arbitrary';
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:23:04 +0200 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Tue, 16 May 2006 21:33:01 +0200 |
wenzelm |
tuned concrete syntax -- abbreviation/const_syntax;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2006 18:51:13 +0200 |
wenzelm |
tuned syntax/abbreviations;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:06 +0200 |
wenzelm |
refined 'abbreviation';
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 21:12:00 +0100 |
wenzelm |
new-style definitions/abbreviations;
|
file |
diff |
annotate
|
| Tue, 03 Jan 2006 15:44:39 +0100 |
paulson |
Provers/classical: stricter checks to ensure that supplied intro, dest and
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:28:43 +0100 |
wenzelm |
tuned induct proofs;
|
file |
diff |
annotate
|
| Fri, 25 Nov 2005 19:09:44 +0100 |
wenzelm |
tuned induct proofs;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2005 22:26:13 +0100 |
wenzelm |
tuned induction proofs;
|
file |
diff |
annotate
|
| Thu, 22 Sep 2005 23:56:15 +0200 |
nipkow |
renamed rules to iprover
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Thu, 10 Feb 2005 17:08:45 +0100 |
berghofe |
Added proof of eta-postponement theorem (using parallel eta-reduction).
|
file |
diff |
annotate
|
| Thu, 30 May 2002 10:12:52 +0200 |
nipkow |
Modifications due to enhanced linear arithmetic.
|
file |
diff |
annotate
|
| Wed, 31 Oct 2001 22:05:37 +0100 |
wenzelm |
tuned notation (degree instead of dollar);
|
file |
diff |
annotate
|
| Fri, 28 Sep 2001 21:45:11 +0200 |
wenzelm |
inductive: no collective atts;
|
file |
diff |
annotate
|
| Mon, 26 Feb 2001 16:36:53 +0100 |
paulson |
minor tweaks to speed the proofs
|
file |
diff |
annotate
|
| Tue, 12 Sep 2000 22:13:23 +0200 |
wenzelm |
renamed atts: rulify to rule_format, elimify to elim_format;
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 21:10:11 +0200 |
wenzelm |
updated attribute names;
|
file |
diff |
annotate
|