--- a/thys/ReStar.thy	Thu Mar 03 08:22:39 2016 +0000
+++ b/thys/ReStar.thy	Sat Mar 05 04:01:10 2016 +0000
@@ -81,8 +81,7 @@
 lemma Der_star [simp]:
   shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
 proof -    
-  have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"
-    
+  have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"  
     by (simp only: star_cases[symmetric])
   also have "... = Der c (A ;; A\<star>)"
     by (simp only: Der_union Der_empty) (simp)