| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Mon, 10 May 2010 15:44:49 +0200 | |
| changeset 2092 | c0ab7451b20d |
| parent 1926 | e42bd9d95f09 |
| permissions | -rw-r--r-- |
|
1890
23e3dc4f2c59
small updates to the paper; remaining points in PAPER-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
_{res} -> _{\textrm{res}} etc.; same for =^{def}?
|
|
23e3dc4f2c59
small updates to the paper; remaining points in PAPER-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
|
|
23e3dc4f2c59
small updates to the paper; remaining points in PAPER-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
Nominal Isabelle view, rather than functional programming view |
|
23e3dc4f2c59
small updates to the paper; remaining points in PAPER-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
(e.g. first sentence of Abstract and Intro) |
|
23e3dc4f2c59
small updates to the paper; remaining points in PAPER-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
|
|
23e3dc4f2c59
small updates to the paper; remaining points in PAPER-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
|
|
23e3dc4f2c59
small updates to the paper; remaining points in PAPER-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
:: for cons might need some explanations, esp. that it's also used later |
|
23e3dc4f2c59
small updates to the paper; remaining points in PAPER-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
next to labels in nominal types (e.g. x::name t::lam). |
|
23e3dc4f2c59
small updates to the paper; remaining points in PAPER-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
|
|
23e3dc4f2c59
small updates to the paper; remaining points in PAPER-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
|
|
23e3dc4f2c59
small updates to the paper; remaining points in PAPER-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
Ott-tool -> Ott tool (throughout) |
|
23e3dc4f2c59
small updates to the paper; remaining points in PAPER-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
|
|
23e3dc4f2c59
small updates to the paper; remaining points in PAPER-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
I didn't quite get top of second column, p. 6 |
|
23e3dc4f2c59
small updates to the paper; remaining points in PAPER-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
|
|
23e3dc4f2c59
small updates to the paper; remaining points in PAPER-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
the equation in the first actuall bullet on p. 8 lacks it =? |
|
23e3dc4f2c59
small updates to the paper; remaining points in PAPER-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
|
|
23e3dc4f2c59
small updates to the paper; remaining points in PAPER-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
missing v. spaces, top of 2nd col p. 8 |