Hi Clemens, > Could you please explain what you mean by "surface context" in the > documentation of the locale command: > >> given bundles take effect in the surface context within both import >> and body and the potentially following begin / end block > > I'm trying to understand where exactly bundles in locale declarations > are effective. I suppose they are not persisted beyond the locale > declaration's begin /end block?
exactly. The surface context is the epheneral hypothetical context on
top of the local theory stack without any permanent effect.
Hope this helps,
Florian
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
