[isabelle-dev] NEWS

[Makarius]

On Tue, 1 Jul 2008, Brian Huffman wrote:

> The merge lets people use any logic image built on HOL together with the 
> complex numbers; this is definitely some thing users should be able to 
> do, but the current solution is a hack and will not scale. I was serious 
> about eventually wanting to use HOL-Word and HOLCF together (it would be 
> very useful for reasoning about Haskell programs that use word types). 
> But I wouldn't be in favor of grafting HOL-Word onto the main HOL image 
> - where would it stop?
> 
> If the merge is intended to be a temporary solution, then that is fine - 
> as long as someone is looking for a better long-term solution.

In the longer term there will be definitely various improvements, based on 
a simplified "session" model (replacing isatool usedir eventually) with 
sane handling of what is now the load path.  Coupling this with writable 
images, the 64bit platform, and mutiprocessing (both in the theory loader 
and user interaction model) there will be a quite different user 
experience.  Only separate compilation is something that I cannot see for 
the future.


	Makarius