Re: [isabelle] Remaining reasons for Proof General

Am 12.11.2013 15:54, 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.

You can define your own abbreviations. F.ex. -, for ¬ :)

Do this by putting the following into ~/.isabelle/etc/symbols

\<not>      code: 0x0000ac  group: logic abbrev: -,
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.