Sat, 26 Apr 2003 12:38:42 +0200 |
paulson |
converting more HOL-Auth to new-style theories
|
file |
diff |
annotate
|
Tue, 08 Oct 2002 08:20:17 +0200 |
nipkow |
Got rid of rotates because of new simplifier
|
file |
diff |
annotate
|
Wed, 03 Oct 2001 20:54:16 +0200 |
wenzelm |
tuned parentheses in relational expressions;
|
file |
diff |
annotate
|
Tue, 08 May 2001 15:57:13 +0200 |
paulson |
fixed a slow proof; tidied
|
file |
diff |
annotate
|
Fri, 23 Mar 2001 12:10:05 +0100 |
paulson |
shortening and streamlining of proofs
|
file |
diff |
annotate
|
Wed, 14 Mar 2001 08:50:55 +0100 |
paulson |
minor tuning
|
file |
diff |
annotate
|
Tue, 27 Feb 2001 16:13:23 +0100 |
paulson |
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
|
file |
diff |
annotate
|
Tue, 13 Feb 2001 13:16:27 +0100 |
paulson |
partial conversion to Isar script style
|
file |
diff |
annotate
|
Tue, 09 Jan 2001 15:29:17 +0100 |
nipkow |
`` -> ` and ``` -> ``
|
file |
diff |
annotate
|
Tue, 30 May 2000 16:08:38 +0200 |
wenzelm |
cleaned up;
|
file |
diff |
annotate
|
Wed, 24 May 2000 18:44:19 +0200 |
paulson |
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
|
file |
diff |
annotate
|
Wed, 19 Apr 2000 11:09:59 +0200 |
paulson |
removal of less_SucI, le_SucI from default simpset
|
file |
diff |
annotate
|
Tue, 07 Sep 1999 10:40:58 +0200 |
wenzelm |
isatool expandshort;
|
file |
diff |
annotate
|
Mon, 06 Sep 1999 18:18:40 +0200 |
oheimb |
added theorems le_maxI1 and le_maxI2, also in claset
|
file |
diff |
annotate
|
Tue, 17 Aug 1999 22:14:02 +0200 |
wenzelm |
HOL_quantifiers;
|
file |
diff |
annotate
|
Tue, 20 Apr 1999 14:33:48 +0200 |
paulson |
addition of Kerberos IV example
|
file |
diff |
annotate
|