# 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 ---------------------------- *)