equal
deleted
inserted
replaced
112 |
112 |
113 \noindent |
113 \noindent |
114 and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of |
114 and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of |
115 type-variables. While it is possible to implement this kind of more general |
115 type-variables. While it is possible to implement this kind of more general |
116 binders by iterating single binders, this leads to a rather clumsy |
116 binders by iterating single binders, this leads to a rather clumsy |
117 formalisation of W. The need of iterating single binders is also one reason |
117 formalisation of W. |
|
118 |
|
119 {\bf add example about W} |
|
120 |
|
121 The need of iterating single binders is also one reason |
118 why Nominal Isabelle and similar theorem provers that only provide |
122 why Nominal Isabelle and similar theorem provers that only provide |
119 mechanisms for binding single variables have not fared extremely well with |
123 mechanisms for binding single variables have not fared extremely well with |
120 the more advanced tasks in the POPLmark challenge \cite{challenge05}, |
124 the more advanced tasks in the POPLmark challenge \cite{challenge05}, |
121 because also there one would like to bind multiple variables at once. |
125 because also there one would like to bind multiple variables at once. |
122 |
126 |