LMF2018: Ejercicios de deducción natural de lógica proposicional con las tácticas de Isabelle/HOL

En la segunda parte de la clase de hoy del curso Lógica matemática y fundamentos se ha explicado las demostraciones en Isabelle/HOL de los ejercicios 1, 2, 3, 5, 22 y 33 de la relación 7.