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 Nunchaku BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices Binomial GCD |
9 imports |
|
10 Predicate_Compile |
|
11 Quickcheck_Narrowing |
|
12 Extraction |
|
13 Nunchaku |
|
14 BNF_Greatest_Fixpoint Filter |
|
15 Conditionally_Complete_Lattices |
|
16 Binomial |
|
17 GCD |
|
18 Nat_Transfer |
10 begin |
19 begin |
11 |
20 |
12 text \<open> |
21 text \<open> |
13 Classical Higher-order Logic -- only ``Main'', excluding real and |
22 Classical Higher-order Logic -- only ``Main'', excluding real and |
14 complex numbers etc. |
23 complex numbers etc. |