Teaching Higher-Order Logic Using Isabelle: A Gentle Introduction to Formal Reasoning in Proof Assistants

The authors present a formalization of higher-order logic in the Isabelle proof assistant, building directly on the foundational Isabelle/Pure framework. The goal is to provide a gentle introduction to higher-order logic and proof assistants, without the complexity of Isabelle/HOL.