000 00386nam a2200133Ia 4500
008 190711s9999 xx 000 0 und d
020 _a3540208542
082 _a511.36 B536
100 _aBERTOT ,Y.
245 0 _aINTERACTIVE THEOREM PROVING AND PROGRAM DEVELOPMENT : COQ ART :CALCULUS OF INDUC
260 _aBERLIN
_bSpringer
_c2004
300 _axxv+469p.,23X15Cms.
942 _cBK
_2DDC
999 _c31899
_d31899