src/HOL/UNITY/Network.ML
changeset 6115 c70bce7deb0f
parent 5648 fe887910e32e
child 6536 281d44905cab
     1.1 --- a/src/HOL/UNITY/Network.ML	Wed Jan 13 12:08:51 1999 +0100
     1.2 +++ b/src/HOL/UNITY/Network.ML	Wed Jan 13 12:16:34 1999 +0100
     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 1);
     1.8 +by (blast_tac (claset() delrules [le0]) 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);