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

[Makarius]

On Wed, 9 Feb 2011, Lawrence Paulson wrote:

> 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.

What issue?  This is about making a non-conservative variation of 
established things, without grasping the consequences yet.

Again: Such things take a long time to understand.  And as always it is a 
matter of priorities where to invest time.  We have many really important 
reforms in the pipeline that need attention.


 	Makarius