[isabelle-dev] Problem in the AFP

Dmitriy Traytel traytel at in.tum.de
Thu Oct 23 15:37:40 CEST 2014


Yes, that's my bad. Thanks! I was about to check Mira for complaints. 
See now AFP/ 1dd93cc85dfb.

Dmitriy

On 23.10.2014 14:25, Florian Haftmann wrote:
> Isabelle 06dfbfa4b3ea
> AFP 33c18a9138e9
>
> *** Unknown old-style datatype "Regular_Exp.rexp"
> *** At command "derive" (line 18 of
> "/mnt/home/haftmann/data/afp/devel/thys/Containers/Compatibility_Containers_Regular_Sets.thy")
>
> 	Florian
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141023/f213632d/attachment-0002.html>


More information about the isabelle-dev mailing list