Shallow-Expressions This is an implementation of shallow expressions in Isabelle/HOL, building on the Optics package.