Wed, 23 Nov 2005 22:26:13 +0100 |
wenzelm |
tuned induction proofs;
|
file |
diff |
annotate
|
Wed, 16 Nov 2005 19:34:19 +0100 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
Fri, 14 Mar 2003 12:02:14 +0100 |
kleing |
fix for changes in HOL/Hoare/
|
file |
diff |
annotate
|
Sat, 09 Nov 2002 00:12:25 +0100 |
kleing |
Hoare.ML -> hoare.ML
|
file |
diff |
annotate
|
Fri, 09 Nov 2001 00:20:26 +0100 |
wenzelm |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
file |
diff |
annotate
|
Tue, 30 Oct 2001 17:37:25 +0100 |
wenzelm |
tuned induct proofs;
|
file |
diff |
annotate
|
Fri, 12 Jan 2001 09:32:53 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 11 Jan 2001 19:36:25 +0100 |
wenzelm |
subst syntax;
|
file |
diff |
annotate
|
Wed, 10 Jan 2001 00:15:33 +0100 |
wenzelm |
use \<acute>;
|
file |
diff |
annotate
|
Mon, 11 Dec 2000 20:11:11 +0100 |
wenzelm |
moved "_update_name" to HOL/Record;
|
file |
diff |
annotate
|
Mon, 06 Nov 2000 22:56:07 +0100 |
wenzelm |
improved: 'induct' handle non-atomic goals;
|
file |
diff |
annotate
|
Tue, 03 Oct 2000 22:39:49 +0200 |
wenzelm |
Hoare logic in Isar;
|
file |
diff |
annotate
|