*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Problem with command-line version*From*: Makarius <makarius at sketis.net>*Date*: Fri, 13 Nov 2009 15:23:58 +0100 (CET)*In-reply-to*: <1968CF58-8E4D-4796-8800-F99D972175EB@uibk.ac.at>*References*: <1968CF58-8E4D-4796-8800-F99D972175EB@uibk.ac.at>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

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 thefollowing error message for the proof step where arith is applied.

Makarius

**References**:**[isabelle] Problem with command-line version***From:*René Thiemann

- Previous by Date: Re: [isabelle] Problem with command-line version
- Next by Date: Re: [isabelle] Does anyone know how to get rid of => marker in PG4.0?
- Previous by Thread: Re: [isabelle] Problem with command-line version
- Next by Thread: [isabelle] Isar macro definitions and polymorphism
- Cl-isabelle-users November 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list