src/Sequents/Modal0.thy
changeset 7098 86583034aacf
parent 2073 fb0655539d05
child 14765 bafb24c150c1
--- a/src/Sequents/Modal0.thy	Tue Jul 27 19:01:46 1999 +0200
+++ b/src/Sequents/Modal0.thy	Tue Jul 27 19:02:43 1999 +0200
@@ -1,10 +1,10 @@
-(*  Title:      Modal/modal0
+(*  Title:      Sequents/Modal0
     ID:         $Id$
     Author:     Martin Coen
     Copyright   1991  University of Cambridge
 *)
 
-Modal0 = LK +
+Modal0 = LK0 +
 
 consts
   box           :: "o=>o"       ("[]_" [50] 50)