equal
deleted
inserted
replaced
1 section \<open>Main HOL\<close> |
1 section \<open>Main HOL\<close> |
2 |
2 |
3 theory Pre_Main |
3 theory Pre_Main |
4 imports Predicate_Compile Quickcheck_Narrowing Extraction Nitpick BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices |
4 imports Predicate_Compile Quickcheck_Narrowing Extraction Nitpick BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices Binomial GCD |
5 begin |
5 begin |
6 |
6 |
7 text \<open> |
7 text \<open> |
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. |