[isabelle-dev] Notes on datatype_new list

Jasmin Blanchette jasmin.blanchette at gmail.com
Mon May 26 13:47:21 CEST 2014

Am 26.05.2014 um 12:05 schrieb Makarius <makarius at sketis.net>:

> The observed here problem is different: the type constructor "list" somehow ends up in the name space with a "concealed" flag.  There might be one or more Binding.conceal too many in the BNF sources.

Ah, now I get it. Of course this is entirely accidental, and I'm surprised we didn't notice before. We'll look into this.


More information about the isabelle-dev mailing list