# HG changeset patch
# User paulson
# Date 845024103 -7200
# Node ID 69bd90345078e7f7486fd40fee36b40b8769b465
# Parent  644104f85d14eac94f49c138fa9c134639da3c51
Addition of Sequents; removal of Modal and LK

diff -r 644104f85d14 -r 69bd90345078 src/Tools/make-all
--- a/src/Tools/make-all	Fri Oct 11 10:52:54 1996 +0200
+++ b/src/Tools/make-all	Fri Oct 11 10:55:03 1996 +0200
@@ -55,7 +55,7 @@
 
 case $FORCE.$EXEC in
   on.on) (cd $ISABELLEBIN;
-          for f in Pure FOL ZF CCL LCF CTT LK Modal HOL HOLCF Cube FOLP
+          for f in Pure FOL ZF CCL LCF CTT Sequents HOL HOLCF Cube FOLP
 	  do 
 	   rm -f $f $f.heap
 	  done)
@@ -121,21 +121,12 @@
 
 echo
 echo
-echo '*****Classical Sequent Calculus (LK)*****'
-(cd LK;  make $NO $TEST > make$$.log)
-tail LK/make$$.log
-gzip LK/make$$.log
-#cannot delete LK yet... it is needed for Modal!
-
-echo
-echo
-echo '*****Modal logic (Modal)*****'
-(cd Modal;  make $NO $TEST > make$$.log)
-tail Modal/make$$.log
-gzip Modal/make$$.log
+echo '*****Sequent Calculi (Sequents)*****'
+(cd Sequents;  make $NO $TEST > make$$.log)
+tail Sequents/make$$.log
+gzip Sequents/make$$.log
 case $CLEAN.$EXEC in
-  on.on)	rm -f $ISABELLEBIN/LK $ISABELLEBIN/LK.heap \
-                      $ISABELLEBIN/Modal $ISABELLEBIN/Modal.heap
+    on.on)	rm -f $ISABELLEBIN/Sequents $ISABELLEBIN/Sequents.heap
 esac
 
 echo
@@ -181,7 +172,7 @@
     test.on)	echo
 	        echo '***** Now check the dates on the "test" files *****'
         	ls -lrt FOL/test ZF/test CCL/test LCF/test CTT/test\
-              	        LK/test Modal/test HOL/test HOLCF/test\
+              	        Sequents/test HOL/test HOLCF/test\
                         Cube/test FOLP/test
 esac
 echo Finished at `date`