src/HOL/Word/WordDefinition.thy
changeset 27139 a1f3c7b5ce9c
parent 27134 71461c77a15b
child 28524 644b62cf678f
equal deleted inserted replaced
27138:63fdfcf6c7a3 27139:a1f3c7b5ce9c
     7 *) 
     7 *) 
     8 
     8 
     9 header {* Definition of Word Type *}
     9 header {* Definition of Word Type *}
    10 
    10 
    11 theory WordDefinition
    11 theory WordDefinition
    12 imports TdThs Size BinBoolList
    12 imports Size BinBoolList TdThs
    13 begin
    13 begin
    14 
    14 
    15 typedef (open word) 'a word
    15 typedef (open word) 'a word
    16   = "{(0::int) ..< 2^len_of TYPE('a::len0)}" by auto
    16   = "{(0::int) ..< 2^len_of TYPE('a::len0)}" by auto
    17 
    17