Building up HOL › Definining Theories [isa-0016]

An Isabelle file is called a theory, and they consist of mathematical definitions (of types and terms), lemmas and proofs. Isabelle theories start with a theory name and a declaration of all the theories on which it depends. The theory name must match the file name, so the code from this lecture should be saved into a file called HOLFromScratch.thy.

theory HOLFromScratch imports Pure begin

We imported the theory Pure, which contains only the very basic built-in structures that define Isabelle's logic.