changeset 149 | e122cb146ecc |
parent 132 | f77a7138f791 |
child 160 | ea2e5acbfe4a |
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*} |