Mario Carneiro (Aug 11 2024 at 04:48): Mario Carneiro (Aug 11 2024 at 04:48):What does the (global) modifier on a theory in a session declaration mean? There seems to be a notion of global vs local theory elsewhere in isabelle (e.g. in global_interpretation) but it's not clear to me if this is the same thing.
Fabian Huch (Aug 12 2024 at 08:04):Those are not the same thing -- global theories are available without further qualification, i.e. you can import the global theory Main but other theories in HOL you'd have to qualify, e.g. HOL.List.
Fabian Huch (Aug 12 2024 at 08:06):You can find the specifiction in Ch. 2.1 in the system manual.
Last updated: Nov 07 2025 at 16:23 UTC