equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* A type of finite bit strings *} |
5 header {* A type of finite bit strings *} |
6 |
6 |
7 theory Word |
7 theory Word |
8 imports Type_Length Misc_Typedef Boolean_Algebra Bool_List_Representation |
8 imports |
|
9 Type_Length |
|
10 Misc_Typedef |
|
11 "~~/src/HOL/Library/Boolean_Algebra" |
|
12 Bool_List_Representation |
9 uses ("~~/src/HOL/Word/Tools/smt_word.ML") |
13 uses ("~~/src/HOL/Word/Tools/smt_word.ML") |
10 begin |
14 begin |
11 |
15 |
12 text {* see @{text "Examples/WordExamples.thy"} for examples *} |
16 text {* see @{text "Examples/WordExamples.thy"} for examples *} |
13 |
17 |