[isabelle-dev] NEWS: Subgoal.FOCUS combinators use anonymous quasi-bound variables

[Makarius]

* Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous
quasi-bound variables (like the Simplifier), instead of accidentally
named local fixes. This has the potential to improve stability of proof
tools, but can also cause INCOMPATIBILITY for tools that don't observe
the proof context discipline.


This refers to Isabelle/e96b7be56d44.

There was nothing really wrong with Subgoal.FOCUS, but after cleanup in 
the vicinity of the new 'subgoal' command, I've found the time might be 
ripe to get to this deterministic naming scheme, according to nesting 
depth of bounds, not accidental "comments" in the Abs nodes.

The change exposed quite odd problems in some existing tools: the above 
"INCOMPATIBILITY for tools that don't observe the proof context 
discipline" does not tell any such story.  The most strange breakdown 
happened in hypsubst.ML, see 03a6b1792cd8.


There is also a discussion about locally invented variable names on the 
thread "HOL-IMP very slow" from 12-Feb-2014, see also 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2014-February/004999.html

Maybe there is a chance to revisit the various the Metis proof 
reconstruction questions from there eventually, in the light of the 
clarified Subgoal.FOCUS discipline.


 	Makarius