01420nam0 22003253i 450 AQ1000787920251003044041.00387582444New York3540582444Berlin20090729d1994 ||||0itac50 baengdez01i xxxe z01nIsabellea generic theorem proverLawrence C. Paulsonwith contributions by Tobias NipkowBerlin [etc.]Springerc1994XVII, 321 p.24 cmLecture notes in computer scienceedited by G. Goos and J. Hartmanis828001MIL00307032001 Lecture notes in computer scienceedited by G. Goos and J. Hartmanis828702 1Goos, GerhardAQ1V006441340511.30285Logica matematica (Logica simbolica). Elaborazione dei dati, applicazioni dell'elaboratore14511.3028553Logica matematica (Logica simbolica). Programmi22Paulson, Lawrence C.MILV07294807062096Nipkow, Tobias <1958- >AQ1V003726ITIT-00000020090729IT-BN0095 AQ10007879Biblioteca Centralizzata di Ateneo193 v. 01COLL. ING. LNCS 0102 0000022455 VMA (0828 v. 828Y 1996021919960219 01Isabelle1381997UNISANNIO