| changeset 48891 | c0eafbd55de3 |
| parent 35113 | 1a0c129bb2e0 |
| child 52143 | 36ffe23b25f8 |
| 48890:d72ca5742f80 | 48891:c0eafbd55de3 |
|---|---|
3 Copyright 1991 University of Cambridge |
3 Copyright 1991 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 theory Modal0 |
6 theory Modal0 |
7 imports LK0 |
7 imports LK0 |
8 uses "modal.ML" |
|
9 begin |
8 begin |
9 |
|
10 ML_file "modal.ML" |
|
10 |
11 |
11 consts |
12 consts |
12 box :: "o=>o" ("[]_" [50] 50) |
13 box :: "o=>o" ("[]_" [50] 50) |
13 dia :: "o=>o" ("<>_" [50] 50) |
14 dia :: "o=>o" ("<>_" [50] 50) |
14 strimp :: "[o,o]=>o" (infixr "--<" 25) |
15 strimp :: "[o,o]=>o" (infixr "--<" 25) |