equal
deleted
inserted
replaced
4 Classical Higher-order Logic -- only ``Main'', excluding real and |
4 Classical Higher-order Logic -- only ``Main'', excluding real and |
5 complex numbers etc. |
5 complex numbers etc. |
6 \<close> |
6 \<close> |
7 |
7 |
8 theory Main |
8 theory Main |
9 imports Predicate_Compile Quickcheck_Narrowing Extraction Nitpick BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices Binomial GCD |
9 imports Predicate_Compile Quickcheck_Narrowing Extraction Nunchaku BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices Binomial GCD |
10 begin |
10 begin |
11 |
11 |
12 text \<open> |
12 text \<open> |
13 Classical Higher-order Logic -- only ``Main'', excluding real and |
13 Classical Higher-order Logic -- only ``Main'', excluding real and |
14 complex numbers etc. |
14 complex numbers etc. |