changeset 35222 | 4f1fba00f66d |
parent 34897 | cf9e3426c7b1 |
child 35284 | 9edc2bd6d2bd |
35221:5cb63cb4213f | 35222:4f1fba00f66d |
---|---|
1 header {* Main HOL *} |
1 header {* Main HOL *} |
2 |
2 |
3 theory Main |
3 theory Main |
4 imports Plain Predicate_Compile Nitpick |
4 imports Plain Predicate_Compile Nitpick Quotient |
5 begin |
5 begin |
6 |
6 |
7 text {* |
7 text {* |
8 Classical Higher-order Logic -- only ``Main'', excluding real and |
8 Classical Higher-order Logic -- only ``Main'', excluding real and |
9 complex numbers etc. |
9 complex numbers etc. |