lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
By chapter:chapters 1 and 2, maybe 3: Peter Whitechapters 6, 7 and 8: David von Oheimchapter 6, maybe 8: Gerwin Kleinchapters 3, maybe 4: Tanja Voschapters 1-3 at least: Stefano Bistarelli