*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Isabelle/jedit*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Mon, 23 Jul 2012 12:14:38 +0900*In-reply-to*: <CAHBFu058aEtrqA22=k2Z8M6VuXEv+e3+uu-KTp9yFOTSTUE-Kw@mail.gmail.com>*References*: <500BDE34.8030100@in.tum.de> <CAAPnxw2wxZbTW5pCNrXxqs+D7voO=nqLvEp89Lkf_+GGXdUh-w@mail.gmail.com> <CAHBFu058aEtrqA22=k2Z8M6VuXEv+e3+uu-KTp9yFOTSTUE-Kw@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:14.0) Gecko/20120717 Thunderbird/14.0

Dear all,

lemma "A & B --> B & A"[] At this point we have the subgoal 1. A ∧ B ⟶ B ∧ A

lamme "A & B --> B & A" []

cheers chris On 07/23/2012 02:42 AM, Fabian Immler wrote:

You could disable "Auto update" in the Output panel and use "Update" manually. Since "Update" is not exported as an action of the Isabelle-Plugin, one cannot assign a keyboard shortcut to see the current proof state. The attached macro (a short hack) emulates a click on "Update" and could be used for an alternative way of interaction: - No "Auto update" - Keyboard shortcut (e.g. Ctrl-Enter) to see the current proof state Installation instructions: - Move the attached update.bsh to ~/.isabelle/Isabelle2012/jedit/macros/ (This script "clicks" on "Update") - Assign a shortcut to this Macro: - either via Utilities->Global Options->Shortcuts (The macro is called "update") - or by appending a line like "update.shortcut=A+ENTER A+m" to ~/.isabelle/Isabelle2012/jedit/properties If this turns out to be a desired/competitive way of interaction, one could think about having these actions exported by the Isabelle-Plugin. Now trying to prove theorems with manual updates of the proof state, Fabian 2012/7/22 Alfio Martini <alfio.martini at acm.org>:Dear Isabelle Users I am also interested in a possible answer to this question. What I usually do in this case is to [repeatedly] move the cursor to the previous [next] line (command, declaration) to take a look at the current proof state before resuming typing or thinking about the current command (declaration). Cheers On Sun, Jul 22, 2012 at 8:04 AM, Tobias Nipkow <nipkow at in.tum.de> wrote:When I start typing in a proof command, eg apply, jedit eagerly executes it, and since I am in the middle of typing it, the command typically fails. Unfortunately the resulting error msg overwrites the proof state. Is there any way to see the old proof state while I type the proof command? Thanks Tobias-- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) Coordenador do Curso de Ciência da Computação Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática 90619-900 -Porto Alegre - RS - Brasil

**References**:**[isabelle] Isabelle/jedit***From:*Tobias Nipkow

**Re: [isabelle] Isabelle/jedit***From:*Alfio Martini

**Re: [isabelle] Isabelle/jedit***From:*Fabian Immler

- Previous by Date: Re: [isabelle] Schematic vars or universal bound vars in theorem?
- Next by Date: Re: [isabelle] [Q]Question about Isabelle/hol
- Previous by Thread: Re: [isabelle] Isabelle/jedit
- Next by Thread: Re: [isabelle] Isabelle/jedit
- Cl-isabelle-users July 2012 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