On Fri, 1 Jan 2016, Lawrence Paulson wrote: > I'm still working on a major theorem. It would be nice to include it if > possible. Do you have a time estimate for that? Makarius