Clean Isabelle formalizations of Anderson's emendation
Add Isabelle verification of Anderson's proposed simplification
Structure paper and write introduction