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



On Tue, Jul 14, 2015 at 10:48 AM, Christian Sternagel <c.sternagel at gmail.com
> wrote:

> 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.)


Thanks! I didn't know I could do that. It looks like in the future I can
use print_options to get a listing of all the current options.


>
>
>     * 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.
>

Yeah that might help a little. It would help more if the detached window
had something connecting it to place it was detached from.

Thanks,
Jason



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