| Tue, 17 Jun 1997 09:01:56 +0200 |
nipkow |
converse -> ^-1
|
file |
diff |
annotate
|
| Wed, 23 Apr 1997 11:18:29 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Sat, 15 Feb 1997 17:52:31 +0100 |
oheimb |
reflecting my recent changes of the simplifier and classical reasoner
|
file |
diff |
annotate
|
| Mon, 07 Oct 1996 10:26:00 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Thu, 26 Sep 1996 12:47:47 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Tue, 10 Sep 1996 20:10:29 +0200 |
nipkow |
Converted proofs to use default clasets.
|
file |
diff |
annotate
|
| Fri, 23 Aug 1996 13:03:02 +0200 |
nipkow |
Generalized my_lemma1: (c3,s3) |--> cs3
|
file |
diff |
annotate
|
| Tue, 07 May 1996 18:19:13 +0200 |
paulson |
Updated for new form of induction rules
|
file |
diff |
annotate
|
| Tue, 30 Apr 1996 17:32:29 +0200 |
nipkow |
Added an equivalence proof which avoids the use of -n->
|
file |
diff |
annotate
|
| Mon, 29 Apr 1996 20:15:33 +0200 |
nipkow |
Streamlined syntax: -(n)-> is now -n->.
|
file |
diff |
annotate
|
| Mon, 29 Apr 1996 15:48:27 +0200 |
nipkow |
Natural and Transition semantics.
|
file |
diff |
annotate
|