Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] local proof context

view this post on Zulip Email Gateway (Aug 19 2022 at 16:58):

From: Buday Gergely <gbuday@karolyrobert.hu>
Hi,

is it true that the local proof context is everything that Query -> Print Context displays? Namely:

context
cases
terms
theorems
state

Cheers

view this post on Zulip Email Gateway (Aug 19 2022 at 16:59):

From: Makarius <makarius@sketis.net>
These are just aspects of the context, except for "state" that is
actually not part of the context.

A context is more than just that, and it can be anything what you need it
to be. See also "implementation" manual section 1.1.

Makarius

Last updated: Nov 21 2024 at 12:39 UTC