* Command 'experiment' opens an anonymous locale context with private
naming policy.
This refers to Isabelle/840d03805755, which also contains more
information.
This is not a joke, but a useful tool to write manuals without polluting
the linear name space of the document, e.g. to explain variants of
specifications.
At the bottom of it is some systematic support for private namings /
bindings with explicit scope. It remains to be seen how much of it will
make be actively used in the release -- with merely 10 years delay.
(March has ended, and we need to make serious steps forward, probably next
week.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
