[isabelle-dev] Remaining uses of Proof General?

Gerwin Klein Gerwin.Klein at nicta.com.au
Fri Jul 25 17:10:21 CEST 2014

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.



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.

More information about the isabelle-dev mailing list