BERTOT ,Y. <br/><br/>
INTERACTIVE THEOREM PROVING AND PROGRAM DEVELOPMENT : COQ ART :CALCULUS OF INDUC 

 - BERLIN  Springer  2004 
 - xxv+469p.,23X15Cms. 
<br/><br/><label>ISBN: </label>3540208542 
<br/><br/><label>Dewey Class. No.: </label>511.36 B536