[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
makarius at sketis.net
Wed Feb 9 11:43:43 CET 2011
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.
More information about the isabelle-dev