Re: [isabelle] refute refutes my simple axiom



On 7/17/2012 4:08 PM, Tjark Weber wrote:

refute simply disregards user-supplied axioms (other than type and
constant definitions). See Section 3.4 (page 52) of
http://user.it.uu.se/~tjawe125/publications/weber08satbased.html
for a brief discussion. As you noticed, this may well lead to spurious
(counter-)models in the presence of such axioms.

I suggest that you use nitpick instead, which -- for all practical
intents and purposes -- is a worthy successor to refute.

Best regards,
Tjark
Tjark,

I like worthy successors.

I had a look at the section you referenced. Thanks.

Regards,
GB





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