# HG changeset patch
# User paulson
# Date 880561008 -3600
# Node ID ed343192de45c76dd96d6027612ca695ff4a87bf
# Parent  451ae21dca28150b6349d275417b2fec433a0a7e
Changes to AddIs improve performance of Blast_tac

diff -r 451ae21dca28 -r ed343192de45 src/HOL/Induct/Comb.ML
--- a/src/HOL/Induct/Comb.ML	Wed Nov 26 16:49:54 1997 +0100
+++ b/src/HOL/Induct/Comb.ML	Wed Nov 26 17:16:48 1997 +0100
@@ -30,7 +30,7 @@
 by (etac rtrancl_induct 1);
 by (Blast_tac 1);
 by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
-                           addSDs [spec_mp]) 1);
+                          addSDs [spec_mp]) 1);
 val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
 
 val [major] = goal Comb.thy "diamond(r) ==> diamond(r^*)";
@@ -102,7 +102,8 @@
 val S_parcontractE = parcontract.mk_cases comb.simps "S =1=> z";
 val Ap_parcontractE = parcontract.mk_cases comb.simps "x#y =1=> z";
 
-AddIs  parcontract.intrs;
+AddSIs [parcontract.refl, parcontract.K, parcontract.S];
+AddIs  [parcontract.Ap];
 AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
 
 (*** Basic properties of parallel contraction ***)