Re: [isabelle] Help file for commands such as "declare [[show_types]]" because jEdit lacks PG features



On 5/25/2012 8:44 PM, Gerwin Klein wrote:
  Lars
Thanks, Lars. I didn't find "find_theorems" in any of the docs, but I found some examples here:
http://www.cse.unsw.edu.au/~cs4161/10s2/Demo12.thy
Chapter 8 of the isar reference manual describes the command, as well as a few other diagnostic commands that may come in handy.

http://isabelle.in.tum.de/dist/Isabelle2012/doc/isar-ref.pdf

The PG menu just passes the string you type to the find_theorems command, it's the same implementation.

Cheers,
Gerwin

Being in the habit of using the Acrobat search is what messed me up. The phrase "find_theorems" is listed in the index, but I had searched on "find", and it didn't show up in the search, so I didn't even think about the index. "Reliable" is the key word; searching on "show types" in Acrobat had found me some "show_types".

Thanks,
GB





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