[isabelle-dev] Remaining uses of Proof General?

René Neumann rene.neumann at in.tum.de
Tue Apr 29 10:17:47 CEST 2014


>> What is funny is that Proof General was actually one of the main
>> reasons of moving only
>> slowly in such token language reforms.
> I am glad that PG still works for most of my theories and I try to keep
> that state as long as feasible. There are already problems with new
> keywords declared by AFP entries that are not listed in the keywords
> file.

'isabelle keywords $SESSION' can be used to generate a new keywords file
with all keywords of $SESSION.

- René
-- 
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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4865 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140429/33e3b04e/attachment.bin>


More information about the isabelle-dev mailing list