| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Wed, 27 Apr 2005 16:41:03 +0200 |
paulson |
minor tidying
|
file |
diff |
annotate
|
| Wed, 10 Jul 2002 16:54:07 +0200 |
paulson |
Fixed quantified variable name preservation for ball and bex (bounded quants)
|
file |
diff |
annotate
|
| Sat, 29 Jun 2002 21:33:06 +0200 |
paulson |
conversion of many files to Isar format
|
file |
diff |
annotate
|
| Mon, 04 Feb 2002 13:16:54 +0100 |
paulson |
New-style versions of these old examples
|
file |
diff |
annotate
|
| Tue, 26 Jun 2001 17:04:54 +0200 |
paulson |
now more like the HOL versions, and with the Square Root example added
|
file |
diff |
annotate
|
| Mon, 21 May 2001 14:36:24 +0200 |
paulson |
X-symbols for set theory
|
file |
diff |
annotate
|
| Mon, 07 Aug 2000 10:29:54 +0200 |
paulson |
instantiated Cancel_Numerals for "nat" in ZF
|
file |
diff |
annotate
|
| Thu, 13 Jun 1996 16:22:37 +0200 |
paulson |
New example of GCDs and divides relation
|
file |
diff |
annotate
|
| Thu, 13 Jun 1996 14:25:45 +0200 |
paulson |
The "divides" relation, the greatest common divisor and Euclid's algorithm
|
file |
diff |
annotate
|