# HG changeset patch
# User urbanc
# Date 1314970217 0
# Node ID 3be00ad980a19c2292c1c964bb9e569219eb3966
# Parent  bc3ffe0dd1d8b023e1716f509106360d4519d3fe
small improvement

diff -r bc3ffe0dd1d8 -r 3be00ad980a1 Closures.thy
--- a/Closures.thy	Fri Sep 02 13:29:46 2011 +0000
+++ b/Closures.thy	Fri Sep 02 13:30:17 2011 +0000
@@ -199,7 +199,7 @@
 qed
 
 lemma cofinite_regular:
-  fixes A::"('a::finite list) set"
+  fixes A::"'a::finite lang"
   assumes "finite (- A)"
   shows "regular A"
 proof -
@@ -278,9 +278,8 @@
   def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}"
   have b: "infinite B"
     unfolding infinite_iff_countable_subset
-    apply(rule_tac x="\<lambda>n. CHR ''a'' ^^^ n" in exI)
-    apply(auto simp add: inj_on_def B_def)
-    done
+    unfolding inj_on_def B_def
+    by (rule_tac x="\<lambda>n. CHR ''a'' ^^^ n" in exI) (auto)
   moreover
   have "\<forall>x \<in> B. \<forall>y \<in> B. x \<noteq> y \<longrightarrow> \<not> (x \<approx>A y)" 
     apply(auto simp add: B_def A_def)