Re: [isabelle] Private/qualified in locales



On 07/07/16 17:15, Lars Hupel wrote:
> 
> is there any shorter way than that to hide a fact in a locale?
> 
> 
> context constructors begin
> context begin (* two contexts for private qualifier *)
> 
>   private lemma seval_correct0:
>     ...
> 
> end
> end
> 

No, this is still the canonical form. At least until the next big reform
in name space management.


	Makarius






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