* 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
