src/HOL/List.thy
changeset 53017 0f376701e83b
parent 53012 cb82606b8215
parent 53015 a1119cf551e8
child 53374 a14d2a854c02
     1.1 --- a/src/HOL/List.thy	Tue Aug 13 16:53:23 2013 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Aug 13 17:45:22 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