On Tue, 29 Nov 2011, Cezary Kaliszyk wrote:
It would be nice to get it fully localized but still the meaning of
typedef that restricts a type fixed in a locale is quite unclear. Or has
this been cleared in the meantime?
Locales are the standard example for a local theory target, but not the
only one.
"Localization" means to conform to certain operations of the generic
context, say when introducing local parameters ("fixes") or working with
implicit polymorphism (via declare_term), and further extra-logical things
like name spaces and notation, and more. There is a spectrum here, and
full localization is an ogoing process, to update things according to the
system APIs of 2008, say; many tools are still stuck in 1998.
Brushed-up interfacing to the infrastructure leads to new possibilities in
the applications.
For the logical part one could also think of AWE as local theory target,
and then one could actually depend on axiomatic parameters and premises in
type definitions.
For the non-logical part, a trivial target like this would help a lot in
writing manuals in a fully formal way, without auxiliary perl patching of
the sources (or generated latex):
example
begin
datatype foo = Foo | Bar foo
definition ...
lemma ...
end
This would merely manage the name spaces, to keep the typical many
variants of similar examples disjoint. Currently one needs workarounds
like foo, foo', foo'', foo\<zeta> etc.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
