src/HOL/Word/WordMain.thy
changeset 27137 d0070c32fdc1
parent 26560 d2fc9a18ee8a
equal deleted inserted replaced
27136:06a8f65e32f6 27137:d0070c32fdc1
    23 
    23 
    24 types word32 = "32 word"
    24 types word32 = "32 word"
    25 types word8 = "8 word"
    25 types word8 = "8 word"
    26 types byte = word8
    26 types byte = word8
    27 
    27 
    28 text {* for more see WordExampes.thy *}
    28 text {* for more see WordExamples.thy *}
    29 
    29 
    30 end
    30 end