Re: [isabelle] Isabelle2015-RC0 available for testing



On Wed, 15 Apr 2015, Lars Hupel wrote:

So far I've noticed a small oddity:

ML‹Local_Theory.note›

The markup produced for the type of this expression is

val it = fn: ?.binding * thm list -> local_theory -> (string * thm list)
* local_theory

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 harmless.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.