Stream: General

Topic: Loading all theories in a large AFP development

view this post on Zulip Gergely Buday (Oct 28 2025 at 14:51):

I would like to import a whole AFP session.

I did use isabelle component -u for the afp directory and for the afp/thys directory. Restarted Isabelle/jEdit.

Still, I cannot do imports "Collections", Isabelle/jEdit complains about

Bad theory import "Draft.Collections"

How can I make this work?

I would like to load the whole AFP session so that I could use theorem search.

view this post on Zulip Fabian Huch (Oct 28 2025 at 14:57):

You cannot import a session. However, many sessions will provide a theory with the same name as the session that has all theories of the session imported.

view this post on Zulip Gergely Buday (Oct 29 2025 at 12:18):

It worked for this session, thanks.

Last updated: Nov 07 2025 at 16:23 UTC