[isabelle] folding and linking in jEdit; curry/split



Dear Isabelle list,

Currently I am working quite a lot on low levels, so I wonder what is
the best way to have theories like Inductive.thy "linked", that is, when
clicking on a lemma, I move to that spot?
I tried setting the base theory to Pure, but then a lot of errors occurred.

Also, is there the possibility to fold exactly the proof of a lemma? In
my current settings only the first line of the statement remains.

On the other hand, regarding the content, I want to show something like

lemma "{ f::'a => 'b . True } \subseteq (UNIV::('a \times 'b ) set)"

I guess the solution uses curry or split in front of f, but I do not see
how.

Best regards,
Henning

Attachment: signature.asc
Description: OpenPGP digital signature



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