On Wed, 9 Feb 2011, Lawrence Paulson wrote:
The simplicity of the new code compared with the old suggests that this
treatment is easier to understand, so we should give it a try.
What do you mean by "give it a try"? Brian has changed long-standing code
within a few hours. Code that has gone through many rounds of refinement
in many years (which are documented in the history). Such things take a
long time to understand, and much longer time to change in a way that does
not cause a lot of collateral damage.
It is interesting that local scopes within structured proofs generate
theorems with nonzero indices, but of course that is a separate matter.
Yes, that is a new aspect that was introduced around 1998/1999.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
