| changeset 69605 | a96320074298 |
| parent 69593 | 3dda49e08b9d |
| child 74302 | 6bc96f31cafd |
| 69604:d80b2df54d31 | 69605:a96320074298 |
|---|---|
5 |
5 |
6 theory Modal0 |
6 theory Modal0 |
7 imports LK0 |
7 imports LK0 |
8 begin |
8 begin |
9 |
9 |
10 ML_file "modal.ML" |
10 ML_file \<open>modal.ML\<close> |
11 |
11 |
12 consts |
12 consts |
13 box :: "o\<Rightarrow>o" ("[]_" [50] 50) |
13 box :: "o\<Rightarrow>o" ("[]_" [50] 50) |
14 dia :: "o\<Rightarrow>o" ("<>_" [50] 50) |
14 dia :: "o\<Rightarrow>o" ("<>_" [50] 50) |
15 Lstar :: "two_seqi" |
15 Lstar :: "two_seqi" |