The Coq mailing list

[Jean-Francois Monin <Jean-Francois.Monin AT imag.fr>]

Hello,

My suggestion is to read the book of Bertot and Casteran : "The Coq'Art".

Regards,
  JF

On Tue, Oct 16, 2007 at 08:37:37AM +0800, 
judy AT mail.ccnu.edu.cn
 wrote:
> Dear Instructors:
> 
> Nowadays I want to practise the tactics and I've got only referrence manual 
> book,
> 
> chapeter 8 is about tactics,but very little examples ,so it is hard to 
> understand
> how to use these tactics,  where can I get some useful little examples 
> focus on
> how to use tactics to proove Lemmas. 
> 
> and I've also got tutorial book,,and found tactics introduced  in tutuorial 
> book
> is not enough to use . 
> 
> please give some recommendation.
> 
> looking forward your help.
> 
> yours Judy.
> 
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> 
> 

-- 
Jean-Francois Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 04 39
F-38610 GIERES                fax (+33 | 0) 4 56 52 04 46