[isabelle-dev] Safe approach to hypothesis substitution

[Makarius]

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 
their scopes.

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)?


 	Makarius