[isabelle-dev] NEWS: command 'experiment'
makarius at sketis.net
Wed Apr 1 23:35:44 CEST 2015
* Command 'experiment' opens an anonymous locale context with private
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