equal
deleted
inserted
replaced
1 header {* Main HOL *} |
1 header {* Main HOL *} |
2 |
2 |
3 theory Main |
3 theory Main |
4 imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick |
4 imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick |
5 BNF_Greatest_Fixpoint |
5 BNF_Greatest_Fixpoint Old_Datatype |
6 begin |
6 begin |
7 |
7 |
8 text {* |
8 text {* |
9 Classical Higher-order Logic -- only ``Main'', excluding real and |
9 Classical Higher-order Logic -- only ``Main'', excluding real and |
10 complex numbers etc. |
10 complex numbers etc. |