Goedel's proof doesn't need S5, KB (resp. MB) is sufficient, the THF and Isabelle files have been modified