Hi Thomas,
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
before.
similarly? :-)))
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...
Best,
Alex
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
