Re: [isabelle] A problem with Auto solve_direct
The assumptions are part of the theorem. After all, nobody would state Fermatâs Last Theorem as
x^n + y^n ~= z^m,
without the preconditions on x, y, z and n.
Regarding your other question: many facts can be proved by simp alone, but here the point is to alert you that your proposed theorem has already been proved in essentially the same form.
> On 6 Jun 2015, at 01:45, W. Douglas Maurer <maurer at gwu.edu> wrote:
> Why does Auto solve_direct tell me that a goal can be solved directly
> with some rule alpha, when this is actually not the case without
> adding using assms?
This archive was generated by a fusion of
Pipermail (Mailman edition) and