equal
deleted
inserted
replaced
67 %%%{\{urbanc, kaliszyk\}@in.tum.de} |
67 %%%{\{urbanc, kaliszyk\}@in.tum.de} |
68 \maketitle |
68 \maketitle |
69 |
69 |
70 \begin{abstract} |
70 \begin{abstract} |
71 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
71 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
72 prover. It provides a proving infrastructure for convenient reasoning about |
72 prover. It provides a proving infrastructure for reasoning about |
73 programming language calculi involving named bound variables (as |
73 programming language calculi involving named bound variables (as |
74 opposed to de-Bruijn indices). In this paper we present an extension of |
74 opposed to de-Bruijn indices). In this paper we present an extension of |
75 Nominal Isabelle for dealing with general bindings, that means |
75 Nominal Isabelle for dealing with general bindings, that means |
76 term-constructors where multiple variables are bound at once. Such general |
76 term-constructors where multiple variables are bound at once. Such general |
77 bindings are ubiquitous in programming language research and only very |
77 bindings are ubiquitous in programming language research and only very |