Fiddled a little with the theorem prover. Managed to move one test case from the "we get this wrong" list to the "we get this right" list. Up to the middle of chapter 5 of "mechanizing proof". I get a bit apathetic when he starts talking about old (ie ~1960s) operating systems military security issues, but it's really a fantastic book. The chapter on the four-color theorem was really interesting. Got french toast at fuel and fuddle, it wasn't very good. If I stop liking their brunch, then I'll really have no reason to go there anymore. I already don't like any of their dinner items very much at all.