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).
Cheers,
Jasmin
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
