Re: [isabelle-dev] Private modifier and qualifiers [was Interpretation in arbitrary targets.]

2013-04-12 Thread Makarius
On Sun, 7 Apr 2013, Clemens Ballarin wrote: Quoting Makarius makar...@sketis.net: On Tue, 26 Mar 2013, Florian Haftmann wrote: Note that we have one more aspect in the back-end that could help here: the 'private' modifier. What would the 'private' modifier do in general? This sounds like

Re: [isabelle-dev] Private modifier and qualifiers [was Interpretation in arbitrary targets.]

2013-04-12 Thread Makarius
On Sun, 7 Apr 2013, Clemens Ballarin wrote: The following may or may not be related: I recently spent some thought on getting rid of the mandatory vs optional distinction of qualifiers. In any case this will likely have considerable impact, so here's the idea: Currently there is the strange

Re: [isabelle-dev] Private modifier and qualifiers [was Interpretation in arbitrary targets.]

2013-04-07 Thread Clemens Ballarin
Quoting Makarius makar...@sketis.net: On Tue, 26 Mar 2013, Florian Haftmann wrote: Note that we have one more aspect in the back-end that could help here: the 'private' modifier. What would the 'private' modifier do in general? This sounds like a new concept. The following may or may