equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header {* Basic Definitions for Binary Integers *} |
8 header {* Basic Definitions for Binary Integers *} |
9 |
9 |
10 theory Bit_Representation |
10 theory Bit_Representation |
11 imports Misc_Numeric Bit |
11 imports Misc_Numeric "~~/src/HOL/Library/Bit" |
12 begin |
12 begin |
13 |
13 |
14 subsection {* Further properties of numerals *} |
14 subsection {* Further properties of numerals *} |
15 |
15 |
16 definition bitval :: "bit \<Rightarrow> 'a\<Colon>zero_neq_one" where |
16 definition bitval :: "bit \<Rightarrow> 'a\<Colon>zero_neq_one" where |