Re: [isabelle] Word authorship



Hi Andreas,

> The main reason
> for creating Native_Word as an AFP entry in the first place was that the
> code_printing declarations therein enlarge the trusted code base. So
> even if Native_Word moves as a whole into the distribution, I think it
> would still be good to keep it separate from the rest of the HOL-Word
> formalization.

Native_Word as a whole has a very clear concept and purpose and it will
definitely remain a separate AFP entry.  Indeed my hope is that there is
room for movement in the opposite direction: move specialized material
from the distribution into the AFP.

Cheers,
	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



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