| changeset 283 | 76caebd18756 |
| parent 0 | a5a9c433f639 |
| child 648 | e27c9ec2b48b |
| 282:731b27c90d2f | 283:76caebd18756 |
|---|---|
2 |
2 |
3 classes term < logic |
3 classes term < logic |
4 |
4 |
5 default term |
5 default term |
6 |
6 |
7 types p,o 0 |
7 types |
8 p |
|
9 o |
|
8 |
10 |
9 arities p,o :: logic |
11 arities |
12 p,o :: logic |
|
10 |
13 |
11 consts |
14 consts |
12 (*** Judgements ***) |
15 (*** Judgements ***) |
13 "@Proof" :: "[p,o]=>prop" ("(_ /: _)" [10,10] 5) |
16 "@Proof" :: "[p,o]=>prop" ("(_ /: _)" [10,10] 5) |
14 Proof :: "[o,p]=>prop" |
17 Proof :: "[o,p]=>prop" |