Re: [isabelle] Hide all constructors of a datatype automatically
On Sat, 14 Dec 2013, Yannick Duchêne (Hibou57) wrote:
May a solution can be found somewhere in “implementation.pdf”, from the
documentation pan. I believe it's possible to modify a theory context
using an embedded SML function (embedded in the theory file), without a
need for modifying Isabelle internal (I'm looking at it, will be back if
I feel I've found anything useful in “implementation.pdf”).
The most relevant section is 1.2.4 Name spaces, especially the "chemical
equation" about binding + naming.
Here is a quick example:
Local_Theory.map_naming (Name_Space.mandatory_path "foo.bar")
definition "a = True"
definition "b = False"
Thus all name bindings that are applied in the context come out with the
This avoids the need to "repair" unintended name space access via the
old-fashioned "hide" operations.
This archive was generated by a fusion of
Pipermail (Mailman edition) and