*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 15:45:24 +0100*In-reply-to*: <528236EB.6050305@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>

Hi, Am Dienstag, den 12.11.2013, 15:10 +0100 schrieb Manuel Eberl: > I must admit I did not know about this option before; it must be rather > new. However, the behaviour is… odd. It seems to complete as soon as > there is only one alternative left, i.e. "\alp" is turned into "α". > "\ta" is turne into "τ". When one types "\alpha", one gets "αha", when > one types "\tau", one gets "τu". So basically, if one wants to use this > feature, one has to remember what part of the abbreviation will lead to > there being only one possibly completion. I believe that that will soon enter your procedural memory. I also just recently switched on this feature and from time to time write Γma, but it becomes less often quickly. With this, entering fancy symbols becomes quite nice. There is still the problem that it relies on unique completions, and some symbols don’t have short unique prefixes, e.g. \sqsubsete is not a great win – but then, this symbol has [=, so I just have to get used to that. 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:*Manuel Eberl

**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

- Previous by Date: Re: [isabelle] Remaining reasons for Proof General
- 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