--- a/thys/Spec.thy	Sat Oct 27 21:36:29 2018 +0100
+++ b/thys/Spec.thy	Wed Jan 02 21:09:33 2019 +0000
@@ -163,7 +163,6 @@
 
 lemma nullable_correctness:
   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
-  apply(induct r)
 by (induct r) (auto simp add: Sequ_def) 
 
 lemma der_correctness: