[isabelle] HOL-Nominal to Isabelle2008



Hi David,

David Streader writes:
 > Hi
 >     I am just rebuilding Isabelle2009. 
 > Unpacking HOL-Nominal_x86-linux.tar.gz  it built directory Isabelle2008 
 > and puts the heaps in there!  
 > Is is safe to move the heaps to Isabelle2009 or is this an old set of heaps?
 > 

I am a bit confused what you want to do, or where
the problem is. HOL-Nominal should be fully integrated
with Isabelle 2009 and should always be up-to-date
with every release since 2009. Indeed, the tar-file 
HOL-Nominal_x86-linux.tar.gz from 

 http://isabelle.in.tum.de/download_x86-linux.html

puts its content to 

 Isabelle2009/heaps/polyml-5.2.1_x86-linux/HOL-Nominal
 Isabelle2009/heaps/polyml-5.2.1_x86-linux/log/HOL-Nominal.gz

Having downloaded the sources for Isabelle 2009, you
should also be able to rebuild the HOL-Nominal package
manually by typing

 ./build -m HOL-Nominal HOL

inside the directory where the Isabelle sources are
located. 

Moving heaps between Isabelle releases, I am sure is
asking for trouble. 

Hope this helps,
Christian





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