src/HOL/List.thy

--- a/src/HOL/List.thy	Mon Mar 29 15:35:04 2004 +0200
+++ b/src/HOL/List.thy	Tue Mar 30 08:45:39 2004 +0200
@@ -331,6 +331,16 @@
 apply (case_tac ys, force, simp)
 done
 
+lemma append_eq_append_conv2: "!!ys zs ts.
+ (xs @ ys = zs @ ts) =
+ (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"
+apply (induct xs)
+ apply fastsimp
+apply(case_tac zs)
+ apply simp
+apply fastsimp
+done
+
 lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)"
 by simp