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


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"

lemma "count M undefined > 0"
  apply transfer
explore - (* Fails. *)

lemma "count M undefined > 0"
  apply (transfer, rename_tac M')
explore - (* Works *)

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