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