--- a/Myhill_1.thy	Wed Feb 16 06:51:58 2011 +0000
+++ b/Myhill_1.thy	Wed Feb 16 12:25:53 2011 +0000
@@ -793,7 +793,7 @@
   def b \<equiv> "rhs - {Trn X r | r. Trn X r \<in> rhs}"
   def B \<equiv> "L b" 
   have "X = B ;; A\<star>"
-  proof-
+  proof -
     have "L rhs = L({Trn X r | r. Trn X r \<in> rhs} \<union> b)" by (auto simp: b_def)
     also have "\<dots> = X ;; A \<union> B"
       unfolding L_rhs_union_distrib[symmetric]