author | nipkow |
Sat, 14 Feb 2004 02:06:12 +0100 | |
changeset 14386 | ad1ffcc90162 |
parent 14385 | 6b15793a641a |
child 14387 | e96d5c42c4b0 |
--- 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)