[isabelle] fast_lin_arith raises Fail



In the attached theory, auto first generates a number of warnings of the from

  Linear arithmetic should have refuted the assumptions.
  Please inform Tobias Nipkow.

before it crashes with an exception Fail
(line 503 of "~~/src/Provers/Arith/fast_lin_arith.ML"):
Linear arithmetic: failed to add thms

Tested with Isabelle2014 and Isabelle2015-RC1.

Best,
Andreas

Attachment: Scratch.thy
Description: application/example



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.