This a complete formalization of Version 2 of Carneades Argument Evaluation Structures (CAES2) in Higher-Ordered Logic (HOL) for the Isabelle proof assistant. CAES2 is the formal model of structured arguments implemented in Version 4 of the Carneades argumentation system. The goal of this formalization is to facilitate machine-checked proofs of theorems about CAES2 properties.