*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Remaining reasons for Proof General*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 12 Nov 2013 15:54:43 +0100*In-reply-to*: <1384267524.2456.10.camel@kirk>*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>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.1.0

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. On 12/11/13 15:45, Joachim Breitner wrote: > 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 > >

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

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

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

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

- 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