Re: [isabelle] Isabelle2015-RC0 available for testing



Hello,

> Any problems, observations etc. can be discussed here on the mailing
> list. Quite often a change of behaviour is perceived as a problem, and
> sometimes it is one, sometimes not.  In any case, open discussion helps
> to figure out what is potentially confusing to users.

I have not worked with RC0 extensively yet. 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. OTOH, if I explicitly
construct a value of that type:

ML‹(@{binding foo}, []): Attrib.binding›

... the markup correctly reports

val it = ("foo", []): Attrib.binding

Cheers
Lars




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