| Fri, 20 Mar 2009 15:24:18 +0100 |
wenzelm |
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
|
| Wed, 11 Jun 2008 15:41:33 +0200 |
wenzelm |
converted ML proofs from simpdata.ML;
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 00:07:05 +0100 |
wenzelm |
removed legacy ML setup;
|
file |
diff |
annotate
|
| Sun, 18 Sep 2005 15:20:08 +0200 |
wenzelm |
converted to Isar theory format;
|
file |
diff |
annotate
|
| Wed, 28 Jul 1999 13:45:33 +0200 |
paulson |
congruence rule for |-
|
file |
diff |
annotate
|
| Tue, 27 Jul 1999 18:52:48 +0200 |
paulson |
a new theory containing just an axiom needed to derive imp_cong
|
file |
diff |
annotate
|
| Tue, 20 Apr 1999 14:38:17 +0200 |
paulson |
IMPORTANT CHANGE: declares class "term". Previously LK (incorrectly)
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 18:17:17 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Wed, 09 Oct 1996 13:32:33 +0200 |
paulson |
New unified treatment of sequent calculi by Sara Kalvala
|
file |
diff |
annotate
|