src/HOL/Library/Diagonal_Subsequence.thy
changeset 57862 8f074e6e22fc
parent 52681 8cc7f76b827a
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/Diagonal_Subsequence.thy	Tue Aug 05 12:42:38 2014 +0200
     1.2 +++ b/src/HOL/Library/Diagonal_Subsequence.thy	Tue Aug 05 12:56:15 2014 +0200
     1.3 @@ -27,8 +27,10 @@
     1.4  
     1.5  lemma subseq_seqseq[intro, simp]: "subseq (seqseq n)"
     1.6  proof (induct n)
     1.7 -  case (Suc n) thus ?case by (subst seqseq.simps) (auto simp: subseq_reduce intro!: subseq_o)
     1.8 -qed (simp add: subseq_def)
     1.9 +  case 0 thus ?case by (simp add: subseq_def)
    1.10 +next
    1.11 +  case (Suc n) thus ?case by (subst seqseq.simps) (auto intro!: subseq_o)
    1.12 +qed
    1.13  
    1.14  lemma seqseq_holds:
    1.15    "P n (seqseq (Suc n))"