[isabelle-dev] Referring to unfolded chained facts

Jasmin Blanchette jasmin.blanchette at gmail.com
Fri Sep 2 16:52:04 CEST 2011


Hi Makarius,

> I have also thought again about 'unfolding' as such: it might actually qualify as preserving textual structure and thus as something that can be included in the textual scope for `...` -- assuming it will someday really cease to perform arbitrary simplification by accident.
> 
> There may well be other ways -- it needs some digging on my universal TODO list.
> 
> 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).

Cheers,

Jasmin




More information about the isabelle-dev mailing list