PAPER-TODO
author Christian Urban <urbanc@in.tum.de>
Sun, 09 May 2010 11:37:19 +0100
changeset 2080 0532006ec7ec
parent 1926 e42bd9d95f09
permissions -rw-r--r--
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