Re: [isabelle] Isabelle2019-RC2: Experience report



Hi Peter,

>  * There are various renamings in HOL-Words, and maybe also simpset
> changes (?). This is not explicitly mentioned by the NEWS entry.

this relates to a post of mine on this mailing list from May 3rd:

> What is relevant for the next release:
> * The traditional entry point HOL-Word.Word is supposed to be
> meta-stable: there might be issues due to things like additional simp
> rules and oscillating full theorem names etc. as not uncommon for new
> releases, but there are no intentional changes in scope there.
> * HOL-Word.More_Word is an additional »sumo« enty point into HOL-Word.
> * Other theories in HOL-Word have undergone a massive internal
> re-structuring and re-grouping of material, absorbing material from AFP
> sessions, particulary Native_Word.

The mere amount of material plus the absence of any deliberate change
made it difficult to distill a conclusive NEWS entry from that.  But if
you have specific observations (e. g. reoccurring proof-breaking
patterns), I am happy to mention them there (or maybe amend HOL-Word
accordingly).

Cheers,
	Florian


Attachment: signature.asc
Description: OpenPGP digital signature



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