| changeset 4024 | 3c056eab237c |
| parent 3942 | 1f1c1f524d19 |
| child 4223 | f60e3d2c81d3 |
| 4023:a9dc0484c903 | 4024:3c056eab237c |
|---|---|
9 *) |
9 *) |
10 |
10 |
11 val banner = "First-Order Logic with Natural Deduction with Proof Terms"; |
11 val banner = "First-Order Logic with Natural Deduction with Proof Terms"; |
12 |
12 |
13 writeln banner; |
13 writeln banner; |
14 |
|
15 reset global_names; |
|
16 |
14 |
17 print_depth 1; |
15 print_depth 1; |
18 |
16 |
19 use_thy "IFOLP"; |
17 use_thy "IFOLP"; |
20 use_thy "FOLP"; |
18 use_thy "FOLP"; |