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();