# HG changeset patch
# User nipkow
# Date 876830352 -7200
# Node ID 834ed1471732d6b4d6847dba5bd55e7f8dafe885
# Parent  a29ab43f71746302711dd85025cff831f125d852
Two lemmas are already in List.

diff -r a29ab43f7174 -r 834ed1471732 src/HOL/TLA/Buffer/Buffer.ML
--- a/src/HOL/TLA/Buffer/Buffer.ML	Tue Oct 14 13:58:47 1997 +0200
+++ b/src/HOL/TLA/Buffer/Buffer.ML	Tue Oct 14 13:59:12 1997 +0200
@@ -8,9 +8,7 @@
 
 (* ---------------------------- Data lemmas ---------------------------- *)
 
-goal List.thy "xs ~= [] --> tl(xs @ ys) = (tl xs) @ ys";
-by (auto_tac (!claset, !simpset addsimps [tl_append,neq_Nil_conv]));
-qed_spec_mp "tl_append2";
+(* "xs ~= [] --> tl(xs @ ys) = (tl xs) @ ys" *)
 Addsimps [tl_append2];
 
 goal List.thy "xs ~= [] --> tl xs ~= xs";
@@ -18,15 +16,7 @@
 qed_spec_mp "tl_not_self";
 Addsimps [tl_not_self];
 
-goal List.thy "!ys zs. (ys @ xs = zs @ xs) = (ys=zs)";
-by (induct_tac "xs" 1);
-by (Simp_tac 1);
-by (REPEAT (rtac allI 1));
-by (subgoal_tac "((ys @ [a]) @ list = (zs @ [a]) @ list) = (ys=zs)" 1);
-by (Asm_full_simp_tac 1);
-by (Blast_tac 1);
-qed_spec_mp "append_same_eq";
-AddIffs [append_same_eq];
+(* "!ys zs. (ys @ xs = zs @ xs) = (ys=zs)" has been subsumed *)
 
 (* ---------------------------- Action lemmas ---------------------------- *)