Re: [isabelle] Isabelle2015-RC0 available for testing
On Wed, 15 Apr 2015, Lars Hupel wrote:
So far I've noticed a small oddity:
The markup produced for the type of this expression is
val it = fn: ?.binding * thm list -> local_theory -> (string * thm list)
I expected to see 'Attrib.binding' there.
This is an odd effect caused by a change in the bootstrap order of
Isabelle/Pure: the ML environment and compiler invocation changes several
times, until it converges to proper Isabelle/ML and theory Pure.
We've occasionally had question marks in Poly/ML type output before, but I
never quite understood the reasons behind it. It is an imperfection, but
This archive was generated by a fusion of
Pipermail (Mailman edition) and