Re: [isabelle] instantiating typedecls with datatypes?



* Makarius <makarius at sketis.net> [2006-11-07 14:34]:
> On Tue, 7 Nov 2006, Tobias Nipkow wrote:
> > > Since the HOL/NI material is for Isabelle2004 only, this won't help you
> > > right now, of course.  Nevertheless, it would be an interesting case-study
> > > to adapt these theories to our forthcoming structuring concepts, but the
> > > non-free license seems to prevent this, i.e. David has to get involved
> > > directly.
> > 
> > Since David specifically says that "any non-commercial use is granted", Thomas
> > is free to use and modify the theories in his research.
> 
> The key question is what happens with the modifications.

I forgot to mention this in my first mail, but I'm working on this as
part of my diploma thesis. David is my tutor and has already expressed
interest in eventually including his theories (noninterference and all
the ism stuff) into Isabelle, so I think we will find a solution to
this.

Are the "structuring concepts" you're referring to already available
in CVS? I'm already adapting all the theories to work with the latest
Isabelle, so I could look into this as well.

Thanks for all your pointers, they really helped me!

Thomas






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