Ce projet vise à mettre à jour et adapter le travail décrit dans la publication "Scalable LCF-style proof translation" de Cezary Kaliszyk et Alexander Krauss, en se concentrant sur l'importation du théorème COMPACT_LS de HOL Light vers Isabelle. Il fournit des instructions pour générer des exports HOL Light et les traiter hors ligne, ainsi que pour importer les preuves dans Isabelle.