| changeset 16417 | 9bc16273c2d4 |
| parent 16121 | a80aa66d2271 |
| child 17276 | 3bb24e8b2cb2 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
5 |
5 |
6 header {* Intuitionistic first-order logic *} |
6 header {* Intuitionistic first-order logic *} |
7 |
7 |
8 theory IFOL |
8 theory IFOL |
9 imports Pure |
9 imports Pure |
10 files ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML") |
10 uses ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML") |
11 begin |
11 begin |
12 |
12 |
13 |
13 |
14 subsection {* Syntax and axiomatic basis *} |
14 subsection {* Syntax and axiomatic basis *} |
15 |
15 |