*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Another newbie question...case-based proofs*From*: Wolfgang Jeltsch <wolfgang-it at jeltsch.info>*Date*: Tue, 12 Mar 2019 18:15:30 +0200*In-reply-to*: <9be127f9-1d5c-9673-3720-e82e46db1e21@gmail.com>*References*: <CAJ=ZMJK4d0xDP4ULTqEFWwXcHdfPN4yLVqRdPV_nht9VHAWbkQ@mail.gmail.com> <2315a38013d645bfa7ed4a7a37948817@chalmers.se> <D296D69F59ADF247B47C452A21D6ED2314142FD6@XMBX3.uibk.ac.at> <1552327215.3710.8.camel@in.tum.de> <9be127f9-1d5c-9673-3720-e82e46db1e21@gmail.com>

Am Dienstag, den 12.03.2019, 09:24 +0100 schrieb Christian Sternagel: > In this session I never even opened either the output or state panels > (neither did I use "apply", for that matter). > > Instead I told students to start from a proof attempt along the lines > of > > by (induction ...) auto > > and then consult the resulting error message (click on the squiggly > underline) for what they might be missing. This means they have to use the mouse and explicitly close error message windows. Such a workflow would be pretty uncomfortable for me. In general, I’d appreciate it a lot if the Isabelle IDE could be made more comfortable for people who mostly use the keyboard and can get on speed with it. In particular, it would be great if the completion mechanism could be improved. Currently you have to wait a bit before you can complete macros for symbols with the tab key. That’s very annoying if you are used to type fluently, because you have to make artificial breaks in your typing. In order to not delay your typing more than necessary, you have the incentive to make those breaks as short as possible, but this may lead to too short a break, with the consequence that you have to delete several characters and start over again. Another problem with the completion mechanism is that a completion list sometimes pops up when you don’t need it (typically after entering a quotation mark), and then you cannot navigate the cursor up or down. Could this situation be improved, or are these things too much wired into jEdit? By the way, have there been any attempts so far to integrate Isabelle into Vim? All the best, Wolfgang

**Follow-Ups**:**Re: [isabelle] Another newbie question...case-based proofs***From:*Nemouchi Yakoub

**Re: [isabelle] Another newbie question...case-based proofs***From:*Peter Lammich

**References**:**[isabelle] Another newbie question...case-based proofs***From:*John F. Hughes

**Re: [isabelle] Another newbie question...case-based proofs***From:*Thomas Sewell

**Re: [isabelle] Another newbie question...case-based proofs***From:*Nagashima, Yutaka

**Re: [isabelle] Another newbie question...case-based proofs***From:*Peter Lammich

**Re: [isabelle] Another newbie question...case-based proofs***From:*Christian Sternagel

- Previous by Date: [isabelle] redistribution of the source code from Isabelle/HOL - legalese
- Next by Date: Re: [isabelle] Another newbie question...case-based proofs
- Previous by Thread: Re: [isabelle] Another newbie question...case-based proofs
- Next by Thread: Re: [isabelle] Another newbie question...case-based proofs
- Cl-isabelle-users March 2019 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