coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Lionel Elie Mamane <lionel AT mamane.lu>
- To: satrajit AT attbi.com
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Using already proved theorems to prove new theorems.
- Date: Tue, 14 Jan 2003 07:10:13 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi,
On Tue, Jan 14, 2003 at 04:52:42AM +0000,
satrajit AT attbi.com
wrote:
> Theorem c:....
> Proof.
> Need to use theorems a and b here so that at the appropriate stage
> in the proof, Auto would simply make use of theorems a and b that
> have been proved already.
Look at section 7.12 of the manual. You want to add a and b to the
"Hints" database used by Auto.
--
Lionel
Attachment:
pgpI0Zs5sp84I.pgp
Description: PGP signature
- [Coq-Club] Using already proved theorems to prove new theorems., satrajit
- Re: [Coq-Club] Using already proved theorems to prove new theorems., Lionel Elie Mamane
Archive powered by MhonArc 2.6.16.