On 25 Jul 2014, at 10:23 am, Makarius <makar...@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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
