Ideally one could select between the standard libraries, the full libraries (everything within HOL) and the AFP by a menu. But there is no need to overcomplicate it the first time. The default should just be HOL/Library. Larry
On 20 Jan 2010, at 11:13, Gerwin Klein wrote: > This would be a good idea, I think. > > Makarius, would we be able to set that up in Munich? It should not require > much maintenance apart from an initial setup and an image from the Isabelle > release. > > We'd still need to think about what set of theories to offer (all of Library, > all sessions, ..). A good selection with not too much in it would probably be > of help to beginners. Too much will confuse more than help.
