changeset 40420 | 552563ea3304 |
parent 40181 | 3788b7adab36 |
child 41919 | e180c2a9873b |
40419:718b44dbd74d | 40420:552563ea3304 |
---|---|
1 header {* Main HOL *} |
1 header {* Main HOL *} |
2 |
2 |
3 theory Main |
3 theory Main |
4 imports Plain Record Predicate_Compile Nitpick |
4 imports Plain Record Predicate_Compile Smallcheck 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. |