LEADER 01420nam0 22003253i 450 
001 AQ10007879
005 20251003044041.0
010   $a0387582444$bNew York
010   $a3540582444$bBerlin
100   $a20090729d1994    ||||0itac50      ba
101 | $aeng
102   $ade
181  1$6z01$ai $bxxxe  
182  1$6z01$an
200 1 $aIsabelle$ea generic theorem prover$fLawrence C. Paulson$gwith contributions by Tobias Nipkow
210   $aBerlin [etc.]$cSpringer$dc1994
215   $aXVII, 321 p.$d24 cm
225 | $aLecture notes in computer science$fedited by G. Goos and J. Hartmanis$v828
410  0$1001MIL0030703$12001 $aLecture notes in computer science$fedited by G. Goos and J. Hartmanis$v828$1702 1$aGoos$b, Gerhard$3AQ1V006441$4340
676   $a511.30285$9Logica matematica (Logica simbolica). Elaborazione dei dati, applicazioni dell'elaboratore$v14
676   $a511.3028553$9Logica matematica (Logica simbolica). Programmi$v22
700  1$aPaulson$b, Lawrence C.$3MILV072948$4070$062096
702  1$aNipkow$b, Tobias$f <1958-    >$3AQ1V003726
801  3$aIT$bIT-000000$c20090729
850   $aIT-BN0095          
912   $aAQ10007879
950  0$aBiblioteca Centralizzata di Ateneo$c193 v.$d 01COLL.     ING.                    LNCS$e 0102 0000022455  VMA   (0828               v. 828$fY $h19960219$i19960219
977   $a 01
996   $aIsabelle$91381997
997   $aUNISANNIO