Myhill_2.thy
changeset 149 e122cb146ecc
parent 132 f77a7138f791
child 160 ea2e5acbfe4a
equal deleted inserted replaced
148:3b7477db3462 149:e122cb146ecc
     1 theory Myhill_2
     1 theory Myhill_2
     2   imports Myhill_1 List_Prefix Prefix_subtract
     2   imports Myhill_1 
       
     3           Prefix_subtract
       
     4           "~~/src/HOL/Library/List_Prefix"
     3 begin
     5 begin
     4 
     6 
     5 section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
     7 section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
     6 
     8 
     7 subsection {* The scheme*}
     9 subsection {* The scheme*}