_{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 equation in the first actuall bullet on p. 8 lacks it =?+
−
+
−
missing v. spaces, top of 2nd col p. 8+
−