changeset 46155 | f27cf421500a |
parent 45990 | b7b905b23b2a |
child 51112 | da97167e03f7 |
46154:5115e47a7752 | 46155:f27cf421500a |
---|---|
1 header {* Main HOL *} |
1 header {* Main HOL *} |
2 |
2 |
3 theory Main |
3 theory Main |
4 imports Plain Predicate_Compile Nitpick More_Set |
4 imports Plain Predicate_Compile 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. |