equal
deleted
inserted
replaced
8 |
8 |
9 consts |
9 consts |
10 box :: "o=>o" ("[]_" [50] 50) |
10 box :: "o=>o" ("[]_" [50] 50) |
11 dia :: "o=>o" ("<>_" [50] 50) |
11 dia :: "o=>o" ("<>_" [50] 50) |
12 "--<",">-<" :: "[o,o]=>o" (infixr 25) |
12 "--<",">-<" :: "[o,o]=>o" (infixr 25) |
|
13 Lstar,Rstar :: "two_seqi" |
|
14 |
|
15 syntax |
13 "@Lstar" :: "two_seqe" ("(_)|L>(_)" [6,6] 5) |
16 "@Lstar" :: "two_seqe" ("(_)|L>(_)" [6,6] 5) |
14 "@Rstar" :: "two_seqe" ("(_)|R>(_)" [6,6] 5) |
17 "@Rstar" :: "two_seqe" ("(_)|R>(_)" [6,6] 5) |
15 Lstar,Rstar :: "two_seqi" |
|
16 |
18 |
17 rules |
19 rules |
18 (* Definitions *) |
20 (* Definitions *) |
19 |
21 |
20 strimp_def "P --< Q == [](P --> Q)" |
22 strimp_def "P --< Q == [](P --> Q)" |