Re: [isabelle] apply x apply y vs. by x y



On 28.07.2015 09:32, Lars Hupel wrote:
>> It is not. I am not sure about proof, but qed usually does a bit more
>> than apply (e.g., solve things by assumption).
> 
> True, but shouldn't that mean that "by xy" solves more than "apply x apply
> y done", instead of the other way round?

I would have expected that, yes. Does "proof x" create the same subgoals
as "apply x"? Does "proof x apply_end y qed" solve the goal?

  -- Lars





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