*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Remaining reasons for Proof General*From*: Joachim Breitner <breitner at kit.edu>*Date*: Tue, 12 Nov 2013 16:09:07 +0100*In-reply-to*: <52824133.5020803@in.tum.de>*References*: <CANofLeJJ8O2Y2ktXUER1AsH1F4CQsBB21PPbLMVVQa-UfwjgoQ@mail.gmail.com> <353FF788-2AA0-4188-8AAD-28E803A1F647@gmail.com> <CANofLeLVT7QWSUE4HhNy+kq9UuCe4J7gsXVEzma0x_SO5C03wQ@mail.gmail.com> <26755B7F-E696-4A5D-9BE7-9BCFA0FF85B8@gmail.com> <alpine.LNX.2.00.1311111227510.20958@macbroy21.informatik.tu-muenchen.de> <5280E51C.3010703@inf.ethz.ch> <alpine.LNX.2.00.1311111531350.10735@macbroy21.informatik.tu-muenchen.de> <52822B89.40809@in.tum.de> <52822EAB.10505@in.tum.de> <5282348B.8040008@in.tum.de> <528236EB.6050305@in.tum.de> <1384267524.2456.10.camel@kirk> <52824133.5020803@in.tum.de>

Hi, Am Dienstag, den 12.11.2013, 15:54 +0100 schrieb Manuel Eberl: > Another problem are codes such as "not", which are still not replaced at > all, since "notation", "note" and so on also exist. I'm afraid I don't > think I can get used to this. for not, I use ~<TAB>. Not consistent with the others, but still fast. In any case I believe that jEdit is an editor capable of suiting most uses when it comes to abbreviations, navigation etc. It surely takes time to find out how things work, and even more how to change the behavior if it does not work as intended, and what fancy plugins are available. Ideally most of the issues that we discussed in this thread about symbols are actually independent from whether we edit Isabelle theories or love letters (\he gives ♡ ;-)), so that we can use upstream resources when solving them. I’m not sure if this is actually the case, though, as I cannot tell which editing features are provided by jEdit by default, which are provided by jEdit but instrumented and configured using the Isabelle plugin, and which are genuine Isabelle plugin features. Greetings, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Remaining reasons for Proof General***From:*Makarius

**References**:**[isabelle] sledgehammer in RC4***From:*Randy Pollack

**Re: [isabelle] sledgehammer in RC4***From:*Jasmin Blanchette

**Re: [isabelle] sledgehammer in RC4***From:*Randy Pollack

**Re: [isabelle] sledgehammer in RC4***From:*Jasmin Blanchette

**Re: [isabelle] sledgehammer in RC4***From:*Makarius

**Re: [isabelle] sledgehammer in RC4***From:*Andreas Lochbihler

**[isabelle] Remaining reasons for Proof General***From:*Makarius

**Re: [isabelle] Remaining reasons for Proof General***From:*Manuel Eberl

**Re: [isabelle] Remaining reasons for Proof General***From:*René Neumann

**Re: [isabelle] Remaining reasons for Proof General***From:*René Neumann

**Re: [isabelle] Remaining reasons for Proof General***From:*Manuel Eberl

**Re: [isabelle] Remaining reasons for Proof General***From:*Joachim Breitner

**Re: [isabelle] Remaining reasons for Proof General***From:*Manuel Eberl

- Previous by Date: [isabelle] jEdit: Theming
- Next by Date: Re: [isabelle] Remaining reasons for Proof General
- Previous by Thread: Re: [isabelle] Remaining reasons for Proof General
- Next by Thread: Re: [isabelle] Remaining reasons for Proof General
- Cl-isabelle-users November 2013 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