Re: [isabelle] Data‑types: How to use discriminators?
On Mon, 09 Dec 2013 10:46:01 +0100, Jasmin Blanchette
<jasmin.blanchette at gmail.com> wrote:
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
I missed it (as it was not my first time in “datatypes.pdf”, I missed this
change in the introduction). Also HOL-BNF can be selected as the default
image in jEdit.
Now there are theorems “t.discI(n)” which indeed do what's needed. The
functions “t.is_Cn” do the same as explicitly defined functions (in a
Is it OK to use HOL-BNF or is it still subject to big change? What would
you recommend between “datatype” and “datatype_new”?
This archive was generated by a fusion of
Pipermail (Mailman edition) and