The file System_A_ESSLLI.thy accompanies the paper Formalizing Henkin-Style Completeness of an Axiomatic System for Propositional Logic (ESSLLI 2020).

The file System_A.thy extends the above with binary conjunction and disjunction operators.

The files System_R.thy and System_W.thy accompany the paper Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL (CICM 2021).

The remaining files accompany the paper More Formalized Axiomatic Systems for Propositional Logic in Isabelle/HOL (SLAI 2022).

Except that the files LT1.thy, LT2.thy, LT3.thy, LT4.thy and CICM.thy are experiments with well-known systems from Jan Lukasiewicz, Alfred Tarski and Carew Arthur Meredith.

See also https://hol.compute.dtu.dk/Systems/