equal
deleted
inserted
replaced
14 \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}} |
14 \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}} |
15 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
15 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
16 \renewcommand{\isasymequiv}{$\dn$} |
16 \renewcommand{\isasymequiv}{$\dn$} |
17 \renewcommand{\isasymiota}{} |
17 \renewcommand{\isasymiota}{} |
18 \renewcommand{\isasymemptyset}{$\varnothing$} |
18 \renewcommand{\isasymemptyset}{$\varnothing$} |
|
19 \newcommand{\LET}{\;\mathtt{let}\;} |
|
20 \newcommand{\IN}{\;\mathtt{in}\;} |
|
21 \newcommand{\END}{\;\mathtt{end}\;} |
|
22 \newcommand{\AND}{\;\mathtt{and}\;} |
19 |
23 |
20 |
24 |
21 |
25 |
22 %----------------- theorem definitions ---------- |
26 %----------------- theorem definitions ---------- |
23 \newtheorem{property}{Property}[section] |
27 \newtheorem{property}{Property}[section] |
39 \maketitle |
43 \maketitle |
40 \begin{abstract} |
44 \begin{abstract} |
41 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
45 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
42 prover. It provides a proving infrastructure for convenient reasoning about |
46 prover. It provides a proving infrastructure for convenient reasoning about |
43 programming language calculi. In this paper we present an extension of Nominal |
47 programming language calculi. In this paper we present an extension of Nominal |
44 Isabelle for dealing with general binding structures. Such binding structures are |
48 Isabelle for dealing with general binding structures. Such binding structures |
45 ubiquitous in programming language research and only very poorly handled by |
49 are ubiquitous in programming language research and only very poorly supported |
46 single binding from the lambda-calculus. We give in this |
50 by theorem provers providing only single binding as in the lambda-calculus. We |
47 paper novel definitions for alpha-equivalence and establish automatically the |
51 give in this paper novel definitions for alpha-equivalence and establish |
48 reasoning structure for alpha-equated terms. For example we provide a strong |
52 automatically the reasoning structure for alpha-equated terms. For example we |
49 induction principle that has the variable convention already built in. |
53 provide a strong induction principle that has the variable convention already |
|
54 built in. |
50 \end{abstract} |
55 \end{abstract} |
51 |
56 |
52 |
57 |
53 \input{session} |
58 \input{session} |
54 |
59 |