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



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

I also found "src/Pure/Tools/find_theorems.ML". I'm trying to study some ML, so maybe I'll figure out completely how to use it from that file.

And there's also a short note in "Isabelle Primer for Mathematicians",
http://dream.inf.ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf

The command is better than the Proof General menu command anyway.

Thanks again,
GB





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