_{res} -> _{\textrm{res}} etc.; same for =^{def}?

Nominal Isabelle view, rather than functional programming view

(e.g. first sentence of Abstract and Intro)

:: for cons might need some explanations, esp. that it's also used later

next to labels in nominal types (e.g. x::name t::lam).

Ott-tool -> Ott tool (throughout)

I didn't quite get top of second column, p. 6

"the problem Pottier and Cheney pointed out": I had forgotten it in the

meantime

the equation in the first actuall bullet on p. 8 lacks it =?

missing v. spaces, top of 2nd col p. 8