Re: [isabelle] make_string



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.

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

"In the same process" means that you can have an editor window open with two theories, one of which imports "ZF", the other imports "Main". Both theories can be edited simultaneously.

It doesn't mean that you can import both into the same theory, which would be very hard indeed.

Cheers
Lars




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