It would be interesting to see how big this would be and how long it would take to build. The idea that the Sumo package is too big to download seems ridiculous nowadays. Perhaps the same logic will apply to us. Larry On 1 Jul 2008, at 22:53, Gerwin Klein wrote: > We could copy xemacs and have a separate HOL-sumo with just > everything in there..