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