[isabelle] sledgehammer, smt and metis
I am currently removing smt from a lot of Isabelle proofs, and I noticed, strictly empirically, what follows.
A number of such proofs kept working by merely (and manually) replacing "by smt" (or "by smt2") with something like "by (metis(no_types,lifting))", (or metis with other combinations of options (e.g., hide_lams, mono_tags, etc...)).
I think that it would be nice, given the licensing issues, that sledgehammer would suggest these alternatives, rather than (or at least in addition to) "by smt".
However, I couldn't find a way of influencing s/h behaviour in such a way, by reading s/h manual.
I tried with smt_proofs=false, to no avail.
Is there a way to attain this result?
This archive was generated by a fusion of
Pipermail (Mailman edition) and