Re: [isabelle] make_string





On 06/24/2018 02:18 AM, Lars Hupel 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.

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

Hi Lars,

Thanks but how do I do this? Does the "editor window" mean the bit on the top left, where I enter things like theory Scratch imports ZF begin?

And how do I do what you are referring to?

If I try

theory Scratch imports ZF begin

ML {* val t = 1 *}

end

theory Scratch imports Main begin

it gives one error message, if I delete the "end" it gives another error message, changing Scratch to Scratch1 makes no difference.

What do I actually do to achieve "have an editor window open with
> two theories, one of which imports "ZF", the other imports "Main""

Thanks.

Jeremy




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