[isabelle-dev] Problems with datatype-new

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Fri Jun 27 10:27:51 CEST 2014

Hi René,

> I have an unexpected problem when defining a datatype using datatype_new.
> theory Test
> imports  
>  "$AFP/Collections/ICF/impl/RBTSetImpl"
> begin
> datatype_new ('a,'b) bar = Foo 'a "'b option" "'b rs"
> Just wanting to report this,

Thank you for your report. This is now fixed (cf. 465ac4021146).



More information about the isabelle-dev mailing list