Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TN has enough examples of the bug.
authornipkow
Sat, 03 Jun 2023 22:54:24 +1000
changeset 78133 0a098088745b
parent 78132 177dae28697b
child 78134 a11ebc8c751a
TN has enough examples of the bug.
src/Provers/Arith/fast_lin_arith.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle