On the Use of Isabelle/HOL for Formalizing New Concise Axiomatic Systems for Classical Propositional Logic Asta Halkjær From and Jørgen Villadsen