diff -r d688a01b8f89 -r 1a4e5b94293b thys/Spec.thy
--- a/thys/Spec.thy	Mon Sep 10 21:41:54 2018 +0100
+++ b/thys/Spec.thy	Sun Sep 30 12:02:04 2018 +0100
@@ -163,6 +163,7 @@
 
 lemma nullable_correctness:
   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
+  apply(induct r)
 by (induct r) (auto simp add: Sequ_def) 
 
 lemma der_correctness: