src/HOL/UNITY/Network.ML
changeset 6676 62d1e642da30
parent 6536 281d44905cab
child 7054 dfd96be49bd9
--- a/src/HOL/UNITY/Network.ML	Fri May 21 10:50:04 1999 +0200
+++ b/src/HOL/UNITY/Network.ML	Fri May 21 10:56:46 1999 +0200
@@ -49,8 +49,8 @@
 by (Clarify_tac 1);
 by (subgoals_tac ["s' (Aproc, Rcvd) = s (Aproc, Rcvd)",
 		  "s' (Bproc, Rcvd) = s (Bproc, Rcvd)"] 1);
-by (REPEAT (blast_tac (claset() addIs [le_anti_sym, le_trans, eq_imp_le]) 2));
-
+by (REPEAT 
+    (blast_tac (claset() addIs [order_antisym, le_trans, eq_imp_le]) 2));
 by (Asm_simp_tac 1);
 result();