*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] using Isabelle programmatically*From*: Viorel Preoteasa <viorel.preoteasa at aalto.fi>*Date*: Thu, 9 Apr 2015 15:41:11 +0300*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

Hello, I am interested in using Isabelle to simplify a formula based on a specific theory. If I would use the Isabelle/jEdit interface I would create a dummy theory theory MySimp imports BaseTheory begin lemma "expression to simplify = A" apply simp At this point the result that I am interested is the left hand-side of the current goal. How can this be done programmatically? Should I use "isabelle_process" or "isabelle console"? Best regards, Viorel Preoteasa

**Follow-Ups**:**Re: [isabelle] using Isabelle programmatically***From:*Lars Hupel

**Re: [isabelle] using Isabelle programmatically***From:*Makarius

- Previous by Date: Re: [isabelle] [Isabelle] how to translate this into Isabelle language to prove the this
- Next by Date: Re: [isabelle] using Isabelle programmatically
- Previous by Thread: Re: [isabelle] Syntax diagram for obtains allows "is" bindings
- Next by Thread: Re: [isabelle] using Isabelle programmatically
- Cl-isabelle-users April 2015 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