equal
deleted
inserted
replaced
1 (* Author: Xingyuan Zhang, Chunhan Wu, Christian Urban *) |
1 (* Author: Xingyuan Zhang, Chunhan Wu, Christian Urban *) |
2 theory Myhill_2 |
2 theory Myhill_2 |
3 imports Myhill_1 "~~/src/HOL/Library/List_Prefix" |
3 imports Myhill_1 List_Prefix |
4 begin |
4 begin |
5 |
5 |
6 section {* Second direction of MN: @{text "regular language \<Rightarrow> finite partition"} *} |
6 section {* Second direction of MN: @{text "regular language \<Rightarrow> finite partition"} *} |
7 |
7 |
8 subsection {* Tagging functions *} |
8 subsection {* Tagging functions *} |