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_setup {*
  Local_Theory.map_naming (Name_Space.mandatory_path "")

definition "a = True"
definition "b = False"


Thus all name bindings that are applied in the context come out with the extra prefix.

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 MHonArc.