TypesTableauxAndGoedelsGod Formalization of Melvin Fitting's Textbook from 2002 in Isabelle/HOL; A semantical embedding in HOL is employed.