This theory is ancient and looks it. It’s also totally unused and probably obsolete. Shall we delete it? Larry -------------- next part -------------- An HTML attachment was scrubbed... URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230110/47581769/attachment.htm>