Finally got a chance to look into replacing the uses of TND in the solutions manual with the new rules. Here's a PR that gives new proofs for a couple of exercises in the TFL section of the book.
It didn't occur to me until after I did a few that we don't have to replace every use of TND, since it's still a derived rule. At least the proof for the exercise in chapter 15 needs to be replaced; but you might want to forget the two commits for the chapter 17 exercises, if you're OK with appeals to \tnd in chapter 17.
rzach
commented
7 years ago
Finally got a chance to look into replacing the uses of TND in the solutions manual with the new rules. Here's a PR that gives new proofs for a couple of exercises in the TFL section of the book.
It didn't occur to me until after I did a few that we don't have to replace every use of TND, since it's still a derived rule. At least the proof for the exercise in chapter 15 needs to be replaced; but you might want to forget the two commits for the chapter 17 exercises, if you're OK with appeals to \tnd in chapter 17.
Should I work on any more of these?