# Re: [isabelle] Generic Contexts and Generic Data

On Tue, 11 Nov 2014, Christian Sternagel wrote:

Until now I used "Local_Theory.declaration" (and applied the obtained morphism to all elements of my "value", which happen to be terms or theorems). Although I have to admit that I'm clueless about the meaning of the "syntax" and "pervasive" flags of "Local_Theory.declaration" (so I just used "false" for both).

Going back to this very abstract level of the original question on this thread: Yes, two times false is fine as a default.

These options correspond to the following variants of declaration commands that are described in the isar-ref manual:

\item @{command "declaration"}~ at {text d} adds the declaration
function @{text d} of ML type @{ML_type declaration}, to the current
local theory under construction.  In later application contexts, the
function is transformed according to the morphisms being involved in
the interpretation hierarchy.

If the @{text "(pervasive)"} option is given, the corresponding
declaration is applied to all possible contexts involved, including
the global background theory.

\item @{command "syntax_declaration"} is similar to @{command
"declaration"}, but is meant to affect only syntactic'' tools by
convention (such as notation and type-checking information).

Makarius

----------------------------------------------------------------------------
http://stop-ttip.org  925,664 people so far
----------------------------------------------------------------------------

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.