changeset 33561 | ab01b72715ef |
parent 33192 | 08a39a957ed7 |
child 33562 | b1e2830ee31a |
33560:b12ab081e5d1 | 33561:ab01b72715ef |
---|---|
1 header {* Main HOL *} |
1 header {* Main HOL *} |
2 |
2 |
3 theory Main |
3 theory Main |
4 imports Plain Nitpick Quickcheck Recdef |
4 imports Plain Nitpick |
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. |