--- a/src/HOL/Library/Diagonal_Subsequence.thy Tue Aug 05 12:42:38 2014 +0200
+++ b/src/HOL/Library/Diagonal_Subsequence.thy Tue Aug 05 12:56:15 2014 +0200
@@ -27,8 +27,10 @@
lemma subseq_seqseq[intro, simp]: "subseq (seqseq n)"
proof (induct n)
- case (Suc n) thus ?case by (subst seqseq.simps) (auto simp: subseq_reduce intro!: subseq_o)
-qed (simp add: subseq_def)
+ case 0 thus ?case by (simp add: subseq_def)
+next
+ case (Suc n) thus ?case by (subst seqseq.simps) (auto intro!: subseq_o)
+qed
lemma seqseq_holds:
"P n (seqseq (Suc n))"