Re: [isabelle] HOL/Auth subgoal (Nonce secrecy)
> 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:
(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