author | paulson |
Mon, 24 May 1999 15:47:36 +0200 | |
changeset 6707 | 3b07e62a718c |
parent 6706 | d8067e272d4f |
child 6708 | 62beb3336b02 |
--- 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";