Re: [isabelle] writing an Isar proof for multiple subgoals
On 07/14/2015 07:30 PM, Jason Dagit wrote:
How did you get isabelle to show you the types? I've been searching for a
way to get this information while using jEdit (without having to C-hover).
you can use
in order to get a list of variables and their types as part of the output.
(Two equivalent forms would be
depending on the context.)
* if you are trying to compare two complicated types for a small
difference it's frustrating that you can't see them on the screen at the
same time. I end up copying and pasting both types from the popup windows
into my buffer to look a them.
Did you know that you can "detach" any popup you obtained via C-hover?
There is a tiny icon in the left-upper corner (right next to the X) for
doing so. This might be useful for comparing different terms.
This archive was generated by a fusion of
Pipermail (Mailman edition) and