Re: [isabelle] make_string





On 06/24/2018 08:40 PM, Makarius wrote:
On 23/06/18 14:58, Jeremy Dawson wrote:

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

See the included ROOT file which defines a session that contains all
theories from HOL + ZF. You can copy that to your project DIRECTORY and
use the session in Isabelle/jEdit as follows:

   isabelle jedit -d DIRECTORY -l "HOL+ZF"

Then you can work with theory ML values from unrelated contexts as
illustrated in the included Scratch.thy, but note that
Thy_Info.get_theory only works for theories loaded into the underlying
session image.


So there is no need to write out string representations of ML values at
all, and try to read them back again (that additional problem has not
even been touch on this thread so far).


	Makarius

Hi Makarius,

Thanks - I tried the above and an extra window appeared containing the following

Build started for Isabelle/HOL+ZF ...
Building HOL+ZF ...

(lots of output here)

*** Failed to load theory "ZF.InfDatatype" (unresolved "ZF.Cardinal_AC")
*** Failed to load theory "ZFC" (unresolved "ZF.InfDatatype")
*** Cannot merge theories with different application syntax
*** At command "theory" (line 10 of "~~/src/ZF/Cardinal_AC.thy")
Unfinished session(s): HOL+ZF
Return code: 2

Session build failed -- prover process remains inactive!

Cheers,

Jeremy




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