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"