Re: [isabelle] instantiating typedecls with datatypes?



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.

Tobias





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