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



On 26/05/2012, at 11:28 AM, gottfried.barrow at gmx.com wrote:

> On 5/24/2012 1:33 AM, Lars Noschinski wrote:
>> On 24.05.2012 02:41, gottfried.barrow at gmx.com wrote:
>>> I was talking about Proof General's feature to search the Isabelle logic
>>> theories for a keyword in the lemma names, theorem names, definition
>>> names, etc.. (Would that be the "Find Theorem" menu command?) I haven't
>>> seen that I can do that in jEdit.
>> You can use the "find_theorems" command for that (which is the same PG uses, but jEdit does not provide a menu item for it).
>> 
>>  -- 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






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