I've only just received this book, but after a few hours I can say that if you want to implement ATP (automated theorem proving) code this book is an excellent choice. It has complete implementations of absolutely everything in OCaml (a dialect of ML, a mostly functional programming language) which is an excellent choice for this type of application. Almost as good as Haskell (I kid.) Chang and Lee is a great book, but forty years have passed...