[isabelle-dev] Safe approach to hypothesis substitution
krauss at in.tum.de
Tue Aug 24 19:50:46 CEST 2010
Thomas Sewell wrote:
> I should clear up some confusion that may have been caused by my
> mail. I was trying to avoid repeating all that had been said on this
> issue, and it seems I left out some that hadn't been said as well.
> This approach avoids ever deleting an equality on a Free variable
> during a 'safe' reasoning step. It will substitute with that equality
> but keep it in place.
Thanks for the clarification. I think I understand better now.
> Note that with this
> change terminal tactics operating in 'unsafe' mode - fast, best, etc
> - will call thin_triv_tac via Context_Rules and behave similarly to
What different behaviour could occur?
> 2. Yes, count vars is a bit strange, as it will consider "(%f. f)
> (%x. x)" to contain two copies of Bound -1. The point is to count
> loose Bounds in the hypotheses as returned by Logic.strip_assums_hyp,
> which it gets right.
So it's probably just the name that confused me...
More information about the isabelle-dev