lan Melville
Date: Tuesday, 21 August 2018 at 06:57
To: "hol-info@lists.sourceforge.net"
Subject: Re: [Hol-info] Assumptions of goal usage
As a more concise question: can you use assumptions of the hypothesis to
eliminate the assumptions of a theorem?
On Mon, Aug 20, 2018,
As a more concise question: can you use assumptions of the hypothesis to
eliminate the assumptions of a theorem?
On Mon, Aug 20, 2018, 4:51 PM Dylan Melville
wrote:
> Let's say I have a goal,
>
> a /\ b /\ c ==> d
>
> and 2 theorems
>
> a /\ b ==> e
>
> e ==> f
>
> All I need to do to solve the
