| changeset 16417 | 9bc16273c2d4 |
| parent 15481 | fc075ae929e4 |
| child 18456 | 8cc35e95450a |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
5 |
5 |
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 files ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") |
10 uses ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") |
11 ("eqrule_FOL_data.ML") |
11 ("eqrule_FOL_data.ML") |
12 ("~~/src/Provers/eqsubst.ML") |
12 ("~~/src/Provers/eqsubst.ML") |
13 begin |
13 begin |
14 |
14 |
15 |
15 |