Companion to Concrete Semantics
Concrete Semantics is a book that teaches the Isabelle proof assistant by having the user implement a simple imperative language.
Unfortunately, the disjoint code snippets set in fancy typography don't make it easy to turn it into running code.
While the entire code for the book is included in the Isabelle installation, going back and forth between the book
and the source can be a bit tedious.
This post aims to make it all clearer.