Re: [isabelle] [Isabelle 2019-RC0] explore/sketch

Hi Dominique,

> explore/sketch fail in certain situations when a variable with the same
> name occurs quantified in the goal, and free in the lemma to be proven
> (as often happens when applying transfer).
> The following example shows this:
> theory Scratch
>   imports Main "HOL-ex.Sketch_and_Explore" "HOL-Library.Multiset"
> begin
> lemma "count M undefined > 0"
>   apply transfer
> explore - (* Fails. *)
> lemma "count M undefined > 0"
>   apply (transfer, rename_tac M')
> explore - (* Works *)

thanks for reporting this.

The upcoming RC2 shall contain which aims to
simulate the eigen context for a printed Isar statement properly.

This is one of the many lingering issues in this PoC implementation.


Attachment: signature.asc
Description: OpenPGP digital signature

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