diff -r 212bfa431fa5 -r 79b37ef9505f Myhill_1.thy --- 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]