diff --git a/docs/base-logic.tex b/docs/base-logic.tex index 5b15171f8a1efccd420206b0bc0a4889d00195ff..a88b58ad7ef575761fa12c94ae74715f6146f8bc 100644 --- a/docs/base-logic.tex +++ b/docs/base-logic.tex @@ -395,7 +395,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda {\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB} \end{mathpar} The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that has to be proven about $a$ and $B$. -\ralf{Trouble is, we don't actually have $\in$ inside the logic...} +%\ralf{Trouble is, we don't actually have $\in$ inside the logic...} \subsection{Consistency} diff --git a/docs/iris.tex b/docs/iris.tex index 1157cfaaace82af50a67b0f4d1d003482f0d3023..ca5b8ff168a3ca08831fc40d54bc08451f6524f3 100644 --- a/docs/iris.tex +++ b/docs/iris.tex @@ -18,7 +18,7 @@ \begin{document} \title{\bfseries The Iris 2.0 Documentation} -%\author{The Iris Team} +\author{\url{http://plv.mpi-sws.org/iris/}} \maketitle \thispagestyle{empty}