diff -r 4d89d4f0ab17 -r 935f183bf406 src/Sequents/ex/Modal/Tthms.ML
--- a/src/Sequents/ex/Modal/Tthms.ML	Fri Feb 05 21:12:45 1999 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(*  Title:      91/Modal/ex/Tthms
-    ID:         $Id$
-    Author:     Martin Coen
-    Copyright   1991  University of Cambridge
-*)
-
-(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
-
-try "|- []P --> P";
-try "|- [](P-->Q) --> ([]P-->[]Q)";    (* normality*)
-try "|- (P--<Q) --> []P --> []Q";
-try "|- P --> <>P";
-
-try "|-  [](P & Q) <-> []P & []Q";
-try "|-  <>(P | Q) <-> <>P | <>Q";
-try "|-  [](P<->Q) <-> (P>-<Q)";
-try "|-  <>(P-->Q) <-> ([]P--><>Q)";
-try "|-        []P <-> ~<>(~P)";
-try "|-     [](~P) <-> ~<>P";
-try "|-       ~[]P <-> <>(~P)";
-try "|-      [][]P <-> ~<><>(~P)";
-try "|- ~<>(P | Q) <-> ~<>P & ~<>Q";
-
-try "|- []P | []Q --> [](P | Q)";
-try "|- <>(P & Q) --> <>P & <>Q";
-try "|- [](P | Q) --> []P | <>Q";
-try "|- <>P & []Q --> <>(P & Q)";
-try "|- [](P | Q) --> <>P | []Q";
-try "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)";
-try "|- (P--<Q) & (Q--<R) --> (P--<R)";
-try "|- []P --> <>Q --> <>(P & Q)";