LMF2017: Ejercicios de deducción natural proposicional en Isabelle/HOL (2)

En la clase de hoy del curso Lógica matemática y fundamentos se han comentado soluciones de ejercicios de deducción natural con Isabelle/HOL. Concretamente, los ejercicios 57 y 58 de la cuarta relación.