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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and