[isabelle-dev] Referring to unfolded chained facts

[Makarius]

On Fri, 2 Sep 2011, Jasmin Blanchette wrote:

>> We should develop some feeling in which direction to move for the 
>> source generation business.  Anyway, is this mission critical for the 
>> upcoming release?
>
> No, not at all. It's not mission critical for any release. I've noticed 
> the problem when running Judgement Day but no user has complained about 
> this yet (and they would quickly realize what went wrong and repair the 
> proof).

I would say we pick up this thread again in fall, after the release.  The 
question of generating robust Isar text is an old one that deserves to be 
addressed more seriously at some point.  (It is also relevant to any kind 
of "proof refactoring" that might come up in the Prover IDE at a later 
stage.)


 	Makarius