Re: [isabelle] Problem with command-line version
On Thu, 12 Nov 2009, René Thiemann wrote:
fix a :: int
have "∃ b. a = a * b ∧ b > 0" by auto
then obtain b where "a = a * b" and "b > 0" by auto
hence "∃ c. b = c + (1 :: int) ∧ c ≥ 0" by arith
hence True by simp
When stepping through the proof interactively, everything works fine.
However, when using isabelle-process (Isabelle 2009), I get the
following error message for the proof step where arith is applied.
Batch mode is a bit more thorough by default, in particular
quick_and_dirty is disabled. Apparently the crash is caused by the full
version of the Cooper procedure, not the oracle version.
It seems that Sasche Böhme has already fixed the problem recently: see
You can direct paste this text into stdin of "patch -p 1", to modify
Alternatively you can make yourself an alpha/beta tester of the next
release, and use one of the many development snapshots. (We are
approaching the next official release already.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and