Re: [isabelle] confusing metis message
The message should be the truth when you have given metis all of HOL.
But since one tends to be a bit more selective, I agree that it is
Now I'm more confused - here it seems that it failed due to not
expanding Domain and Range, and so (even given all of HOL) would
My "all of HOL" was meant to include all your definitions.
But, in any case, your remark suggests I've misunderstood what a
typical invocation would be, or what it already knows?
Metis knows first-order logic. Everything else you have to tell it. In
contrast to blast. Hence metis is primarily useful in connection with
sledgehammer, which figures out the required lemmas for you.
This archive was generated by a fusion of
Pipermail (Mailman edition) and