| changeset 15019 | acf67fa30998 |
| parent 14156 | 2072802ab0e3 |
| child 15481 | fc075ae929e4 |
| 15018:0a84ca4e0f90 | 15019:acf67fa30998 |
|---|---|
5 |
5 |
6 header {* Classical first-order logic *} |
6 header {* Classical first-order logic *} |
7 |
7 |
8 theory FOL = IFOL |
8 theory FOL = IFOL |
9 files |
9 files |
10 ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") |
10 ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML"): |
11 ("simpdata.ML") ("FOL_lemmas2.ML"): |
|
12 |
11 |
13 |
12 |
14 subsection {* The classical axiom *} |
13 subsection {* The classical axiom *} |
15 |
14 |
16 axioms |
15 axioms |