[isabelle-dev] Quotient example with partiality?
makarius at sketis.net
Wed Nov 30 11:21:27 CET 2011
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
"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
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
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):
datatype foo = Foo | Bar foo
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.
More information about the isabelle-dev