# HG changeset patch # User nipkow # Date 1031584032 -7200 # Node ID daefa3ac893376d8f5e52434751f455b92a818ca # Parent d9651081578ba9db811bf38bdf24aa668d4ef04d bug in counter example finder diff -r d9651081578b -r daefa3ac8933 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Sat Sep 07 22:04:28 2002 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Mon Sep 09 17:07:12 2002 +0200 @@ -181,7 +181,7 @@ fun ratmin2(r,s) = if ratle(r,s) then r else s; fun ratmax2(r,s) = if ratle(r,s) then s else r; -val ratmin = foldr1 ratmax2; +val ratmin = foldr1 ratmin2; val ratmax = foldr1 ratmax2; fun ratroundup r = let val (p,q) = rep_rat r