[isabelle-dev] Remaining uses of Proof General?

[Gerwin Klein]

On 25 Jul 2014, at 10:23 am, Makarius <makarius at sketis.net> wrote:

> Oddly, people are still seen using 'find_theorems' etc. inlined into the source text.  That was an intermediate approach from several years ago. If it is still used today, what are the remaining resons for it?

Not having to touch the mouse is the main reason for me why I still use thm, find_theorems, sledgehammer etc commands.

Cheers,
Gerwin

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.