| changeset 24365 | 038b164edfef |
| parent 24364 | 31e359126ab6 |
| child 24383 | e4582c602294 |
| 24364:31e359126ab6 | 24365:038b164edfef |
|---|---|
7 in particular, bin_rec and related work |
7 in particular, bin_rec and related work |
8 *) |
8 *) |
9 |
9 |
10 header {* Basic Definitions for Binary Integers *} |
10 header {* Basic Definitions for Binary Integers *} |
11 |
11 |
12 theory BinGeneral imports TdThs Num_Lemmas |
12 theory BinGeneral imports Num_Lemmas |
13 |
13 |
14 begin |
14 begin |
15 |
15 |
16 subsection {* Recursion combinator for binary integers *} |
16 subsection {* Recursion combinator for binary integers *} |
17 |
17 |