# HG changeset patch
# User berghofe
# Date 1263143351 -3600
# Node ID b23bd3ee4813319e7fc289664cb1a445a249039b
# Parent  a799687944af75724cae223f5d99828660ac90d0
same_append_eq / append_same_eq are now used for simplifying induction rules.

diff -r a799687944af -r b23bd3ee4813 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Jan 10 18:06:30 2010 +0100
+++ b/src/HOL/List.thy	Sun Jan 10 18:09:11 2010 +0100
@@ -578,13 +578,13 @@
 apply fastsimp
 done
 
-lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)"
+lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)"
 by simp
 
 lemma append1_eq_conv [iff]: "(xs @ [x] = ys @ [y]) = (xs = ys \<and> x = y)"
 by simp
 
-lemma append_same_eq [iff]: "(ys @ xs = zs @ xs) = (ys = zs)"
+lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)"
 by simp
 
 lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])"