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 ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and