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

[Lawrence Paulson]

I mean, let's see how many proofs are affected (including the AFP obviously) by this proposed change. If there are many incompatibilities, then we need to look at other ways of dealing with this issue. It should be done on somebody's local copy, of course.
Larry

On 9 Feb 2011, at 10:11, Makarius wrote:

> 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