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).


          925,664 people so far

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