On 21.05.2013 13:59, Makarius wrote:
I do this usually by searching backwards for "context" (which means I
might miss contexts opened by "locale") or manually search through the
sidekick. To check whether I am in a local context at all, I usually
insert an additional "end" command and look for an error.
BTW, there is also the old-fashioned TTY command print_context to ask
the prover. It is more relevant in non-trivial contexts like
'interpretation'. On the other hand, all these things should be more
immediate in the Prover IDE, as generated templates or similar.
I did not know about print_context, which solves my immediate use case.
This command is not documented in the reference manual (at least not in
the index), though. Also, it only seems to work half-way for unnamed
contexts:
- If I open an unnamed context with some fixes, assumes in the theory
context, print_context ignores this, i.e. in
theory Foo imports Main begin
context fixes P assumes P begin
print_context outputs only "theory Foo".
- This is different inside a named context:
theory Foo imports Main begin
locale A begin
context fixes P assumes P begin
yields
theory Foo
locale A =
fixes P :: "bool"
assumes "P"
as output of print_context. Although this might also be considered
slightly irritating, as those elements are not part of the locale,
so something like
theory Foo
locale A
context
fixes P :: "bool"
assumes "P"
would be better.
How is interpretation related to print_context? It seems that neither
interpret nor interpretation extends the context as displayed by
print_context?
-- Lars
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
