Re: [isabelle] writing an Isar proof for multiple subgoals



Dear Jason,

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

  declare [[show_types=true]]

in order to get a list of variables and their types as part of the output.

(Two equivalent forms would be

  using [[show_types=true]]

and

  from [[show_types=true]]

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.

cheers

chris




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