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
http://isabelle.in.tum.de/repos/isabelle/rev/129757af1096 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.

Cheers,
	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



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