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


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

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

end


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