Re: [isabelle] instantiating typedecls with datatypes?



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.


	Makarius






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