[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution

[Makarius]

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