| Wed, 11 Jul 2007 11:14:51 +0200 |
berghofe |
Adapted to new inductive definition package.
|
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
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
| Thu, 24 Oct 2002 07:23:46 +0200 |
nipkow |
ASIN -> SET
|
file |
diff |
annotate
|
| Tue, 08 Oct 2002 08:20:17 +0200 |
nipkow |
Got rid of rotates because of new simplifier
|
file |
diff |
annotate
|
| Fri, 26 Apr 2002 11:47:01 +0200 |
nipkow |
New machine architecture and other direction of compiler proof.
|
file |
diff |
annotate
|
| Thu, 20 Dec 2001 18:22:44 +0100 |
nipkow |
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
|
file |
diff |
annotate
|
| Wed, 19 Dec 2001 00:26:04 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 09 Dec 2001 14:34:56 +0100 |
kleing |
tuned for latex output
|
file |
diff |
annotate
|
| Fri, 23 Nov 2001 17:19:14 +0100 |
nipkow |
Isar conversion
|
file |
diff |
annotate
|
| Sat, 06 Oct 2001 00:02:46 +0200 |
wenzelm |
* sane numerals (stage 2): plain "num" syntax (removed "#");
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Mon, 30 Apr 2001 19:26:04 +0200 |
nipkow |
new proof
|
file |
diff |
annotate
|
| Fri, 10 Nov 2000 09:17:54 +0100 |
nipkow |
JMB -> JMPB. Email von Johannes Pfeifroth.
|
file |
diff |
annotate
|
| Thu, 26 Oct 2000 14:59:38 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 26 Oct 2000 14:52:41 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|