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
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,

I like worthy successors.

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


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