Re: [isabelle] make_string





On 06/22/2018 11:46 PM, Makarius wrote:
Isabelle/ZF and Isabelle/HOL can coexist happily within the same
Isabelle/ML process: Isabelle2017 has already introduced a reform on
theory names to make them globally unique accross all Isabelle + AFP
sessions.

Hi Makarius,

How so?  When I try
theory Scratch imports ZF Main begin
I get an error message

Jeremy




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