delrules [r_into_rtrancl] required because the new I-rule made a step slow.
There must be others somehwere...

--- a/src/HOL/BCV/JVM.ML	Thu Oct 12 12:16:58 2000 +0200
+++ b/src/HOL/BCV/JVM.ML	Thu Oct 12 12:18:51 2000 +0200
@@ -187,10 +187,11 @@
 by (Asm_simp_tac 1);
 
 by (rtac conjI 1);
-by (fast_tac (claset() addss (simpset() addsplits [list.split])) 1);
+by (force_tac (claset(), simpset() addsplits [list.split]) 1);
 
 by (rtac conjI 1);
-by (fast_tac (claset() addDs [rtrancl_trans]
+by (fast_tac (claset() delrules [r_into_rtrancl]
+		       addDs [rtrancl_trans]
        addss (simpset() addsplits [list.split])) 1);
 
 by (rtac conjI 1);