Re: [isabelle] Local_Theory.map_naming in locales



On Wed, 18 Feb 2015, Makarius wrote:

So far, the "naming" of a local_theory only refers to the background theory for foundation. There is still no provision for more name space control, but it is one of the important things in the pipeline for a very long time. Over many years, there were just important ingredients missing to move forward, e.g. unnamed context begin ... end blocks. There were also rather lame reasons like the inability to write "private definition ..." or "private theorem ..." with TTY/Proof General still around.

This thread about Isabelle name space policies is continued on isabelle-dev, just in the nick of time before the hot phase of the Isabelle2015 process starts.

The "lame reasons" due to TTY/Proof General no longer exist ...


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.