src/HOL/List.thy
changeset 53015 a1119cf551e8
parent 52435 6646bb548c6b
child 53017 0f376701e83b
     1.1 --- a/src/HOL/List.thy	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Aug 13 16:25:47 2013 +0200
     1.3 @@ -2095,13 +2095,13 @@
     1.4  done
     1.5  
     1.6  lemma append_eq_append_conv_if:
     1.7 - "(xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =
     1.8 -  (if size xs\<^isub>1 \<le> size ys\<^isub>1
     1.9 -   then xs\<^isub>1 = take (size xs\<^isub>1) ys\<^isub>1 \<and> xs\<^isub>2 = drop (size xs\<^isub>1) ys\<^isub>1 @ ys\<^isub>2
    1.10 -   else take (size ys\<^isub>1) xs\<^isub>1 = ys\<^isub>1 \<and> drop (size ys\<^isub>1) xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>2)"
    1.11 -apply(induct xs\<^isub>1 arbitrary: ys\<^isub>1)
    1.12 + "(xs\<^sub>1 @ xs\<^sub>2 = ys\<^sub>1 @ ys\<^sub>2) =
    1.13 +  (if size xs\<^sub>1 \<le> size ys\<^sub>1
    1.14 +   then xs\<^sub>1 = take (size xs\<^sub>1) ys\<^sub>1 \<and> xs\<^sub>2 = drop (size xs\<^sub>1) ys\<^sub>1 @ ys\<^sub>2
    1.15 +   else take (size ys\<^sub>1) xs\<^sub>1 = ys\<^sub>1 \<and> drop (size ys\<^sub>1) xs\<^sub>1 @ xs\<^sub>2 = ys\<^sub>2)"
    1.16 +apply(induct xs\<^sub>1 arbitrary: ys\<^sub>1)
    1.17   apply simp
    1.18 -apply(case_tac ys\<^isub>1)
    1.19 +apply(case_tac ys\<^sub>1)
    1.20  apply simp_all
    1.21  done
    1.22