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.

Larry Paulson

> On 6 Jun 2015, at 01:45, W. Douglas Maurer <maurer at> 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 MHonArc.