# HG changeset patch
# User paulson
# Date 927553656 -7200
# Node ID 3b07e62a718c007eaf7193846e4aadc658fcae98
# Parent  d8067e272d4f18355ea1b32240f671364aef7098
using generic rules when possible

diff -r d8067e272d4f -r 3b07e62a718c src/HOL/UNITY/LessThan.ML
--- a/src/HOL/UNITY/LessThan.ML	Mon May 24 15:47:06 1999 +0200
+++ b/src/HOL/UNITY/LessThan.ML	Mon May 24 15:47:36 1999 +0200
@@ -138,7 +138,7 @@
 (*** Combined properties ***)
 
 Goal "atMost n Int atLeast n = {n}";
-by (blast_tac (claset() addIs [le_anti_sym]) 1);
+by (blast_tac (claset() addIs [order_antisym]) 1);
 qed "atMost_Int_atLeast";