This advanced hands-on course will introduce the Isabelle proof environment, and specifically the theorem-proving facilities within Higher Order Logic. Participants will first learn how to perform proofs in HOL, exploring both the interactive environment and existing proof strategies in Isabelle. They will then have a chance to explore the meta-logic and learn how different object logics are written into Isabelle and how proof strategies for such new logics can be programmed.