Schulz_Leon_Formalizations-in-Isabelle