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

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
similarly fail, and announce invalidity, if the lemma involved some
other user-defined constant?

But, in any case, your remark suggests I've misunderstood what a
typical invocation would be, or what it already knows?

best,
Peter





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