| changeset 24097 | 86734ba03ca2 |
| parent 23154 | 5126551e378b |
| child 24830 | a7b3ab44d993 |
| 24096:74926cdbf071 | 24097:86734ba03ca2 |
|---|---|
6 header {* Classical first-order logic *} |
6 header {* Classical first-order logic *} |
7 |
7 |
8 theory FOL |
8 theory FOL |
9 imports IFOL |
9 imports IFOL |
10 uses |
10 uses |
11 "~~/src/Provers/classical.ML" |
|
12 "~~/src/Provers/blast.ML" |
|
13 "~~/src/Provers/clasimp.ML" |
|
11 ("cladata.ML") |
14 ("cladata.ML") |
12 ("blastdata.ML") |
15 ("blastdata.ML") |
13 ("simpdata.ML") |
16 ("simpdata.ML") |
14 begin |
17 begin |
15 |
18 |