Re: [isabelle] Undefined facts in skip_proofs mode
On Thu, 31 Jul 2014, Gerwin Klein wrote:
I’m surprised that latex output works with it at all, for instance. It
is even possible in some cases that the theorems you get out of
skip_proofs are slightly different to the ones you would get from a
It would be nice to do skip_proofs properly. For instance, I could
imagine that judicious use of futures may supersede the current
I am trying to do such reforms for years. Eventually it should be all
just one uniform concept to manage forked proofs, potentially with
different priorities and different policies to insist or not insist in
joining them later.
To get there, the usual layers of sediments need to be cleaned up slowly
and steadily. Moreover, one needs to have a clear picture of typical
applicaions, beyond accidental features inherited from the past.
That is why it is important to describe particular situations in a
meaningful way. Often the reports are isomorphic to "I want to use
feature X in the context of Y, but it fails".
This archive was generated by a fusion of
Pipermail (Mailman edition) and