src/HOLCF/IOA/NTP/Impl.ML

   by (forward_tac [rewrite_rule [Impl.inv1_def]
                                (inv1 RS invariantE) RS conjunct1] 1);
   by (rtac impI 1);
   by (rtac impI 1);
   by (REPEAT (etac conjE 1));
-  by (dres_inst_tac [("k","count (rsch s) (~sbit(sen s))")] le_imp_add_le 1);
+  by (dres_inst_tac [("m","count (rsch s) (~sbit(sen s))")] trans_le_add1 1);
   by (Asm_full_simp_tac 1);
 
   (* 1 *)
   by (tac2 1);
   by (forward_tac [rewrite_rule [Impl.inv1_def]
                                (inv1 RS invariantE) RS conjunct2] 1);
   by (rtac impI 1);
   by (rtac impI 1);
   by (REPEAT (etac conjE 1));
   by (fold_tac  [rewrite_rule[Packet.hdr_def]Impl.hdr_sum_def]);
-  by (dres_inst_tac [("k","hdr_sum (srch s) (sbit(sen s))")] le_imp_add_le 1);
+  by (dres_inst_tac [("m","hdr_sum (srch s) (sbit(sen s))")] trans_le_add1 1);
   by (Asm_full_simp_tac 1);
 qed "inv2";
 
 
 (* INVARIANT 3 *)