[isabelle-dev] Safe approach to hypothesis substitution
makarius at sketis.net
Wed Aug 25 13:29:57 CEST 2010
On Wed, 25 Aug 2010, Andreas Schropp wrote:
> What does this say about our equality-elimination criterion, which wants
> to check if there are any assumptions involving a Free?
It does not want to check that, and the version by Thomas does not do it.
In fact his approach looks like going in the right direction.
Going back tp that, it has already been mentioned that goal parameters
(bounds) can somehow be treated as private to the proof state, while frees
can reach back into the context arbitraily. In fact, a Free is just like
a local Const in most situations, i.e. Free/Const are only different in
Is there any chance to get a practically useful version of hypsubst that
does not distinguish local constants (Free) from constants of the
background theory (Const)?
More information about the isabelle-dev