| changeset 66954 | 0230af0f3c59 |
| parent 66817 | 0b12755ccbb2 |
| child 67385 | deb9b0283259 |
| 66953:826a5fd4d36c | 66954:0230af0f3c59 |
|---|---|
13 Nunchaku |
13 Nunchaku |
14 BNF_Greatest_Fixpoint Filter |
14 BNF_Greatest_Fixpoint Filter |
15 Conditionally_Complete_Lattices |
15 Conditionally_Complete_Lattices |
16 Binomial |
16 Binomial |
17 GCD |
17 GCD |
18 Nat_Transfer |
|
19 begin |
18 begin |
20 |
19 |
21 text \<open> |
20 text \<open> |
22 Classical Higher-order Logic -- only ``Main'', excluding real and |
21 Classical Higher-order Logic -- only ``Main'', excluding real and |
23 complex numbers etc. |
22 complex numbers etc. |