src/HOL/Library/Word.thy
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15325 50ac7d2c34c9
equal deleted inserted replaced
15139:58cd3404cf75 15140:322485b816ac
     4 *)
     4 *)
     5 
     5 
     6 header {* Binary Words *}
     6 header {* Binary Words *}
     7 
     7 
     8 theory Word
     8 theory Word
     9 import Main
     9 imports Main
    10 files "word_setup.ML"
    10 files "word_setup.ML"
    11 begin
    11 begin
    12 
    12 
    13 subsection {* Auxilary Lemmas *}
    13 subsection {* Auxilary Lemmas *}
    14 
    14