Re: [isabelle] Data‑types: How to use discriminators?



Hi Yannick,

> Also I noticed “datatypes.pdf” talks about “datatype_new” and some others, which seems not to be recognized. Is this an error or something old or something new to come?

The answer is in the introduction of that document (p. 4):

 To use the package, it is necessary to import the BNF theory, which can be precompiled into the HOL-BNF image. The following commands show how to launch jEdit/PIDE with the image loaded and how to build the image without launching jEdit:

    isabelle jedit -l HOL-BNF
    isabelle build -b HOL-BNF

Regards,

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.