changeset 41959 | b460124855b8 |
parent 39159 | 0dec18004e75 |
child 42814 | 5af15f1e2ef6 |
41958:5abc60a017e0 | 41959:b460124855b8 |
---|---|
1 (* Title: Modal/S43.thy |
1 (* Title: Sequents/S43.thy |
2 Author: Martin Coen |
2 Author: Martin Coen |
3 Copyright 1991 University of Cambridge |
3 Copyright 1991 University of Cambridge |
4 |
4 |
5 This implements Rajeev Gore's sequent calculus for S43. |
5 This implements Rajeev Gore's sequent calculus for S43. |
6 *) |
6 *) |