changeset 6456 | 23602e214ebf |
parent 3839 | 56544d061e1d |
child 7094 | 6f18ae72a90e |
6455:34c6c2944908 | 6456:23602e214ebf |
---|---|
9 (eta-expanded, beta-contracted) |
9 (eta-expanded, beta-contracted) |
10 *) |
10 *) |
11 |
11 |
12 LK = Sequents + |
12 LK = Sequents + |
13 |
13 |
14 classes |
|
15 term < logic |
|
16 |
|
17 default |
|
18 term |
|
14 |
19 |
15 consts |
20 consts |
16 |
21 |
17 Trueprop :: "two_seqi" |
22 Trueprop :: "two_seqi" |
18 "@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5) |
23 "@Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5) |