Concrete Semantics
Theory Files
- Download files for Part I, Isabelle
- Part II, Semantics:
- All IMP theories are in the Isabelle distribution in the directory
src/HOL/IMP.
- You can import a specific theory, say file
T.thy, into your
own Isabelle theory like this:
imports "~~/src/HOL/IMP/T"
- Click here for a pdf and an html version of these theories.