# HG changeset patch
# User nipkow
# Date 902400501 -7200
# Node ID 5a29c309b0b7301405364a817b7b25fc1560ef53
# Parent  70f478d5560640c70bbc0d9c5a8816dc154c7e3b
Lemma renamed in HOL.

diff -r 70f478d55606 -r 5a29c309b0b7 src/HOLCF/IOA/NTP/Impl.ML
--- a/src/HOLCF/IOA/NTP/Impl.ML	Thu Aug 06 12:46:38 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Impl.ML	Thu Aug 06 12:48:21 1998 +0200
@@ -194,7 +194,7 @@
   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 *)
@@ -205,7 +205,7 @@
   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";