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)