Re: [isabelle] make_string

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).

session "HOL+ZF" = HOL + sessions ZF theories ZFC
theory Scratch
  imports Pure

ML \<open>
  val Main_thy = Thy_Info.get_theory "Main";
  val ZF_thy = Thy_Info.get_theory "ZF";


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