[isabelle-dev] HOL/Word

[Gerwin Klein]

Someone (Florian, I guess) thought it was a good idea to have "one unified Word theory" as the commit log says. I heartily disagree, but whatever. 

What I find vexing is that some word lemmas have disappeared in Isabelle2011 and there is no mention of any such thing in NEWS or commit logs. And the patch that seems to be responsible (hg id 56e3520b68b2) is a humongous blob roughly twice the size of the original word library (once removing it, once re-adding some but not all bits of it munged into one file).

Does anyone know what's going on? Do I really have to figure out precisely which are gone and then reprove them? 

Is anyone prepared to leak Florian's new email address so I may haunt him?

Gerwin