Re: [isabelle] Clash of conversion rules at interpretation command

Brian Huffman wrote:
Unfortunately, there doesn't seem to be a way to undeclare the pred_set_conv attribute, so I don't see a workaround.

If your theory does not depend on R being a set, a workaround would be to
use inductive (which does not need pred_set_conv) instead of inductive_set.


Dr. Stefan Berghofer               E-Mail: berghofe at
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY  

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