| changeset 38393 | 7c045c03598f |
| parent 36899 | bcd6fce5bf06 |
| child 40121 | e7a80c6752c9 |
| 38392:8a3ca8b96b23 | 38393:7c045c03598f |
|---|---|
1 header {* Main HOL *} |
1 header {* Main HOL *} |
2 |
2 |
3 theory Main |
3 theory Main |
4 imports Plain Predicate_Compile Nitpick SMT |
4 imports Plain Record Predicate_Compile Nitpick SMT |
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. |