theory Foo imports Main begin locale L begin definition foo where "foo = True" end (* Comment or uncomment the following to observe changes in theory Bar. *) interpretation L . end