changeset 149 | e122cb146ecc |
parent 132 | f77a7138f791 |
child 160 | ea2e5acbfe4a |
--- a/Myhill_2.thy Tue Mar 15 15:53:22 2011 +0000 +++ b/Myhill_2.thy Wed Mar 23 12:17:30 2011 +0000 @@ -1,5 +1,7 @@ theory Myhill_2 - imports Myhill_1 List_Prefix Prefix_subtract + imports Myhill_1 + Prefix_subtract + "~~/src/HOL/Library/List_Prefix" begin section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}