added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
_{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+ −