--- a/src/Provers/Arith/fast_lin_arith.ML Fri Jun 02 12:14:17 2023 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Sat Jun 03 22:54:24 2023 +1000
@@ -499,8 +499,7 @@
(tracing (cat_lines
(["Assumptions:"] @ map (Thm.string_of_thm ctxt) asms @ [""] @
["Proved:", Thm.string_of_thm ctxt fls, ""]));
- warning "Linear arithmetic should have refuted the assumptions.\n\
- \Please inform Tobias Nipkow.")
+ warning "Linear arithmetic should have refuted the assumptions but failed to.")
in finish ctxt' hyps fls end
handle FalseE (thm, hyps, ctxt') =>
trace_thm ctxt ["False reached early:"] (finish ctxt' hyps thm)