changeset 14386 | ad1ffcc90162 |
parent 14372 | 51ddf8963c95 |
child 14510 | 73ea1234bb23 |
--- a/src/Provers/Arith/fast_lin_arith.ML Thu Feb 12 00:28:23 2004 +0100 +++ b/src/Provers/Arith/fast_lin_arith.ML Sat Feb 14 02:06:12 2004 +0100 @@ -550,9 +550,7 @@ \but could not construct a counter example either.\n\ \Probably the proposition is true but cannot be proved\n\ \by the incomplete decision procedure.") - end - handle NotYetImpl => - tracing "No counter example: < on real not yet implemented."; + end; fun mknat pTs ixs (atom,i) = if LA_Logic.is_nat(pTs,atom)