equal
deleted
inserted
replaced
3 Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson |
3 Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson |
4 *) |
4 *) |
5 |
5 |
6 header {* The basis of Higher-Order Logic *} |
6 header {* The basis of Higher-Order Logic *} |
7 |
7 |
8 theory HOL = CPure |
8 theory HOL |
9 files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML"): |
9 import CPure |
10 |
10 files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") |
|
11 begin |
11 |
12 |
12 subsection {* Primitive logic *} |
13 subsection {* Primitive logic *} |
13 |
14 |
14 subsubsection {* Core syntax *} |
15 subsubsection {* Core syntax *} |
15 |
16 |