Myhill_2.thy
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"} *}