# HG changeset patch
# User paulson
# Date 932563074 -7200
# Node ID dfd96be49bd99e8e1d2f2a997910b2c92b84a337
# Parent  8f246bc87ab2d78c4203ad904ef6932cb65de5a3
a more robust proof

diff -r 8f246bc87ab2 -r dfd96be49bd9 src/HOL/UNITY/Network.ML
--- a/src/HOL/UNITY/Network.ML	Wed Jul 21 15:17:30 1999 +0200
+++ b/src/HOL/UNITY/Network.ML	Wed Jul 21 15:17:54 1999 +0200
@@ -45,7 +45,7 @@
 by (dtac ([rs_AB, nondec_idle] MRS constrains_Int RS constrainsD) 1);
 by (assume_tac 1);
 by (ALLGOALS Asm_full_simp_tac);
-by (blast_tac (claset() delrules [le0]) 1);
+by (blast_tac (HOL_cs addIs [order_refl]) 1);
 by (Clarify_tac 1);
 by (subgoals_tac ["s' (Aproc, Rcvd) = s (Aproc, Rcvd)",
 		  "s' (Bproc, Rcvd) = s (Bproc, Rcvd)"] 1);