[isabelle-dev] NEWS: command 'experiment'

Makarius makarius at sketis.net
Wed Apr 1 23:35:44 CEST 2015

* Command 'experiment' opens an anonymous locale context with private
naming policy.

This refers to Isabelle/840d03805755, which also contains more 

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 

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 


More information about the isabelle-dev mailing list