# HG changeset patch
# User paulson
# Date 1021288921 -7200
# Node ID adb0c97883cf1826bb6e6e329f2f4bef8a9ab27e
# Parent  1ebd8ed5a1a01e74fe0f462b8beea168072d4fc8
Deleting two simprules saves 21 seconds!

diff -r 1ebd8ed5a1a0 -r adb0c97883cf src/ZF/List.ML
--- a/src/ZF/List.ML	Mon May 13 11:05:27 2002 +0200
+++ b/src/ZF/List.ML	Mon May 13 13:22:01 2002 +0200
@@ -470,19 +470,19 @@
 qed "append_left_is_self_iff2";
 Addsimps [append_left_is_self_iff2];
 
+(*TOO SLOW as a default simprule!*)
 Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> \
 \  length(ys)=length(zs) --> (xs@ys=zs <-> (xs=Nil & ys=zs))";
 by (etac list.induct 1);
 by (auto_tac (claset(), simpset() addsimps [length_app]));
 qed_spec_mp "append_left_is_Nil_iff";
-Addsimps [append_left_is_Nil_iff];
 
+(*TOO SLOW as a default simprule!*)
 Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> \
 \  length(ys)=length(zs) --> (zs=ys@xs <-> (xs=Nil & ys=zs))";
 by (etac list.induct 1);
 by (auto_tac (claset(), simpset() addsimps [length_app]));
 qed_spec_mp "append_left_is_Nil_iff2";
-Addsimps [append_left_is_Nil_iff2];
 
 Goal "xs:list(A) ==> ALL ys:list(A). \
 \     length(xs)=length(ys) --> (xs@us = ys@vs) <-> (xs=ys & us=vs)";
@@ -536,7 +536,7 @@
 Addsimps [append1_eq_iff];
 
 Goal "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)";
-by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [append_left_is_Nil_iff]) 1);
 qed "append_right_is_self_iff";
 Addsimps [append_right_is_self_iff];