src/Provers/Arith/fast_lin_arith.ML
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)