| changeset 31203 | 5c8fb4fd67e0 |
| parent 29825 | ab97183f1694 |
| child 33192 | 08a39a957ed7 |
| 31202:52d332f8f909 | 31203:5c8fb4fd67e0 |
|---|---|
1 header {* Main HOL *} |
1 header {* Main HOL *} |
2 |
2 |
3 theory Main |
3 theory Main |
4 imports Plain Code_Eval Map Recdef SAT |
4 imports Plain Quickcheck Map Recdef SAT |
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. |