| changeset 14854 | 61bdf2ae4dc5 |
| parent 6509 | 9f7f4fd05b1f |
| child 17480 | fd19f77dcf60 |
| 14853:8d710bece29f | 14854:61bdf2ae4dc5 |
|---|---|
8 |
8 |
9 IFOLP = Pure + |
9 IFOLP = Pure + |
10 |
10 |
11 global |
11 global |
12 |
12 |
13 classes term < logic |
13 classes term |
14 |
|
15 default term |
14 default term |
16 |
15 |
17 types |
16 types |
18 p |
17 p |
19 o |
18 o |
20 |
|
21 arities |
|
22 p,o :: logic |
|
23 |
19 |
24 consts |
20 consts |
25 (*** Judgements ***) |
21 (*** Judgements ***) |
26 "@Proof" :: "[p,o]=>prop" ("(_ /: _)" [51,10] 5) |
22 "@Proof" :: "[p,o]=>prop" ("(_ /: _)" [51,10] 5) |
27 Proof :: "[o,p]=>prop" |
23 Proof :: "[o,p]=>prop" |