[isabelle-dev] Notes on datatype_new list
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