changeset 8263 | 699d4ad2ced3 |
parent 7582 | 2650c9c2ab7f |
child 9073 | 40d8dfac96b8 |
--- a/src/Provers/Arith/fast_lin_arith.ML Fri Feb 18 20:27:19 2000 +0100 +++ b/src/Provers/Arith/fast_lin_arith.ML Sat Feb 19 13:47:12 2000 +0100 @@ -194,13 +194,13 @@ | extract xs [] = (None,xs) in extract [] end; - +(*? fun print_ineqs ineqs = writeln(cat_lines(""::map (fn Lineq(c,t,l,_) => string_of_int c ^ (case t of Eq => " = " | Lt=> " < " | Le => " <= ") ^ commas(map string_of_int l)) ineqs)); - +!*) fun elim ineqs = let (*?val dummy = print_ineqs ineqs;!*)