[isabelle-dev] NEWS

[Florian Haftmann]

* Self-contained library theory "Word" taken over from former session
"HOL-Word".

* Former session "HOL-Word": Misc ancient material has been factored out
into separate theories and moved to session Word_Lib in the AFP.  See
theory "Guide" there for further information.  INCOMPATIBILITY.

This refers to Isabelle/c7038c397ae3 and AFP/1d9680ca2b5.

I finally decided to take this step already before the next release
since the division between HOL-Word and Word_Lib is historical and
artificial and prevents organisation of the existing material.

Currently I plan some more streamlining, particularly more telling
theory names, which will be reflected in Guide.thy accordingly.

With Isabelle2021 planned for February 2021, there is still some time
for early adopters to have a look at the current matter of affairs.

Cheers,
	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20201029/fa65ecef/attachment.sig>