Re: [isabelle] HOL/Auth subgoal (Nonce secrecy)

Hi Denis,

> Sledgehammer suggested a metis command which resulted in an Ill-typed
> instantiation error.

I'll let others answer the rest of your email, but when this happens one solution is to try passing the "full_types" option to Sledgehammer:

    sledgehammer [full_types]

(See the manual sledgehammer.pdf for details.) Then the encoding used is somewhat heavier but is much less likely to cause metis failures.



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