[isabelle-dev] NEWS: command 'experiment'

[Makarius]

* 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