equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header {* Definition of Word Type *} |
8 header {* Definition of Word Type *} |
9 |
9 |
10 theory WordDefinition |
10 theory WordDefinition |
11 imports Type_Length Misc_Typedef BinBoolList |
11 imports Type_Length Misc_Typedef Bool_List_Representation |
12 begin |
12 begin |
13 |
13 |
14 subsection {* Type definition *} |
14 subsection {* Type definition *} |
15 |
15 |
16 typedef (open word) 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}" |
16 typedef (open word) 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}" |