Re: [isabelle] Performance considerations of locales



On 22/09/2021 13:34, Makarius wrote:
> 
> Maybe you can rephrase most of this directly with the 'def' command from
> https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/Pure/ex/Def.thy;f79dfc7656ae
> (it should also work with current Isabelle2021).

See also the adjacent examples:
https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/Pure/ex/Def_Examples.thy;f79dfc7656ae


	Makarius




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