src/HOL/Library/Sublist.thy
changeset 59997 90fb391a15c1
parent 58881 b9556a055632
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/Sublist.thy	Fri Apr 10 11:31:10 2015 +0200
     1.2 +++ b/src/HOL/Library/Sublist.thy	Fri Apr 10 11:52:55 2015 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4  
     1.5  lemma take_prefix: "prefix xs ys \<Longrightarrow> prefix (take n xs) ys"
     1.6    apply (induct n arbitrary: xs ys)
     1.7 -   apply (case_tac ys, simp_all)[1]
     1.8 +   apply (case_tac ys; simp)
     1.9    apply (metis prefix_order.less_trans prefixI take_is_prefixeq)
    1.10    done
    1.11