Building Isabelle Proofs

Todo

An example doing verification. Maybe focus on how to write the Makefile for verification and code generation, rather on the Isabelle proofs themselves.