These are the points of Alan's second part of corrections 
that J may help to solve:



page 57:

J wrote:
"Some collections of rewrite lemmas can cause \THM's rewriter not to terminate."
Alan asks:
"How is this indicated to the user and how does the user deal with it?"
CP guesses: 
"Time out (if at all) + removing "rewrite tags" after analysis of run."



page 70:

footnote 164:
I wrote something on the flamboyant (imho) and sloppy (matter of fact)
language of some of Alan's papers.
This note was a bit over the top, but served an important function in a
paper whose audience will consist mosty of logicians and historians,
who have a tendency to welcome a "logical" treatment of the field
of heuristics more than it would be appropriate.

The footnote read:
"While Christoph Walther is well aware of the primacy of testing in 
 [Walther, 1992; 1993], 
 this awareness is not reflected in the sloppy language 
 of the most interesting papers [Stevens, 1988]
 and [Bundy et al., 1989]: 
 A “rational reconstruction” or “meta-theoretic analysis” of heuristics
 does not make sense in our opinion, and heuristics cannot be “bugged” 
 or “have serious flaws”,
 but can only turn out to be inferior to others w.r.t. a standard corpus."

Alan Bundy remarked:
"But the term 'bug' or 'flaw' may refer to some failure of the heuristic 
 on that corpus and try to explain the reasons for that failure."

CP does not like the word "reasons" in this context,
because it is not correct in philosophical terms.

The footnote now reads:
"While Christoph Walther is well aware of the primacy of testing in 
 [Walther, 1992; 1993],
 this awareness is not reflected in the sloppy language 
 of the most interesting papers [Stevens, 1988] 
 and [Bundy et al., 1989]: 
 Heuristics cannot be “bugged” or “have serious flaws”, 
 unless this would mean that they turn out to be inferior to others 
 w.r.t. a standard corpus. 
 A “rational reconstruction” or a “meta-theoretic analysis” 
 may help to guess even superior heuristics, 
 but they do not have any epistemological value per se."

Is that okay?