changeset 29820 | 07f53494cf20 |
parent 29304 | 5c71a6da989d |
child 29888 | ab97183f1694 |
29802:d201a838d0f7 | 29820:07f53494cf20 |
---|---|
1 header {* Main HOL *} |
1 header {* Main HOL *} |
2 |
2 |
3 theory Main |
3 theory Main |
4 imports Plain Code_Eval Map Nat_Int_Bij Recdef |
4 imports Plain Code_Eval Map Nat_Int_Bij 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. |