1.1 --- a/src/HOL/UNITY/Network.ML Wed Jul 21 15:17:30 1999 +0200
1.2 +++ b/src/HOL/UNITY/Network.ML Wed Jul 21 15:17:54 1999 +0200
1.3 @@ -45,7 +45,7 @@
1.4 by (dtac ([rs_AB, nondec_idle] MRS constrains_Int RS constrainsD) 1);
1.5 by (assume_tac 1);
1.6 by (ALLGOALS Asm_full_simp_tac);
1.7 -by (blast_tac (claset() delrules [le0]) 1);
1.8 +by (blast_tac (HOL_cs addIs [order_refl]) 1);
1.9 by (Clarify_tac 1);
1.10 by (subgoals_tac ["s' (Aproc, Rcvd) = s (Aproc, Rcvd)",
1.11 "s' (Bproc, Rcvd) = s (Bproc, Rcvd)"] 1);