Re: [isabelle] Isabelle2019-RC2: Experience report



On 14/05/2019 13:46, Peter Lammich wrote:
> 
>  * The ML-Level interface of intro_locales_tac changed. The new 
>   "strict" and "eager" flags are not documented at all, I figured out
> the right combination for me by trial and error.

The relevant change for Locale.intro_locales_tac is here:
https://isabelle.sketis.net/repos/isabelle-release/rev/0c1d7a414185 --
it should make clear how to upgrade this rarely used operation.

(Recall that the outdated terminology of "ML-level" is leading to
misunderstandings about the true structure of Isabelle. It should be
possible to get rid of it eventually, 10 years after it became out of
proper use.)


	Makarius




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