On Mon, 9 Aug 2010, Lucas Dixon wrote:
I was wondering about that also.
Is there conceptual reason that "Local_Theory.target" is needed, or is
it just kind of technical hiccup?
These low-level functional adaptions of variations on Context.generic are
mostly for internal use only. This applies to ProofContext.theory,
Local_Theory.theory, Local_Theory.target etc. alike.
declaration {* fn phi => Data.map (Integer.add 3) *}
Local_Theory.declaration (or 'declaration' in Isar syntax) is the standard
way. Of course, the morphism phi must not be ignored in general -- it
needs to be applied to your data as explained in the paper by
Chaieb/Wenzel (CALCULEMUS 2007).
While it is unlikely that integer parameters can be passed through
morphisms in a sensible way, it is mandatory for standard logical entities
(types, terms, facts). Otherwise the declaration will only work in the
global context, where the morphism is identity.
In many practical situations the somewhat simpler 'declare' form with
user-defined attributes turns out more convenient. When using the
standard context parsers Args.typ, Args.term, Attrib.thm etc. the system
takes care of the gory details, i.e. it is correct my canonical
construction (in most situations).
Also note that plain bool/int/string parameters can be managed as
"configuration options". Then the declaration business is all managed by
the system.
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
