On Sun, Jul 29, 2012 at 7:11 PM, Makarius <makar...@sketis.net> wrote: > The question is if HOL-Plain and HOL-Main still have any purpose. Full HOL > now takes < 2min on a reasonably fast machine with 4 cores.
Images like HOL-Plain or HOL-Main are often useful when I am doing development on libraries within the HOL image. Building these images saves me a lot of time, because otherwise I would have to load the same set of files repeatedly in Proof General, which can take several minutes on my (old, not-reasonably-fast, 2-core) machine. Of course, if we can make it easy enough to build custom images, then there is no practical reason to have HOL-Plain or HOL-Main set up by default in the distribution. - Brian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
