--- a/Myhill_2.thy	Sun Feb 20 17:47:54 2011 +0000
+++ b/Myhill_2.thy	Sun Feb 20 18:54:31 2011 +0000
@@ -801,6 +801,9 @@
   shows "finite (UNIV // \<approx>(L r))"
 by (induct r) (auto)
 
+theorem Myhill_Nerode:
+  shows "(\<exists>r::rexp. A = L r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
+using Myhill_Nerode1 Myhill_Nerode2 by metis
 
 (*
 section {* Closure properties *}
@@ -811,9 +814,6 @@
   "reg A \<equiv> \<exists>r::rexp. A = L r"
 
 
-theorem Myhill_Nerode:
-  shows "reg A \<longleftrightarrow> finite (UNIV // \<approx>A)"
-using Myhill_Nerode1 Myhill_Nerode2 by auto
 
 lemma closure_union[intro]:
   assumes "reg A" "reg B"