Pg. 145: > There is an analogous in the Isabelle/HOL standard library Here, a word seems to be missing after 'analogous' Pg. 150: > performs chained rewriting using facts arithmetic should be "arithmetic facts"