equal
deleted
inserted
replaced
74 \author{Cezary Kaliszyk} |
74 \author{Cezary Kaliszyk} |
75 \address{University of Tsukuba, Japan} |
75 \address{University of Tsukuba, Japan} |
76 \email{kaliszyk@cs.tsukuba.ac.jp} |
76 \email{kaliszyk@cs.tsukuba.ac.jp} |
77 \thanks{$^\star$~This is a revised and expanded version of~\cite{UrbanKaliszyk11}} |
77 \thanks{$^\star$~This is a revised and expanded version of~\cite{UrbanKaliszyk11}} |
78 |
78 |
79 \keywords{Nominal Isabelle, variable convention, theorem provers, formal reasoning,lambda-calculus} |
79 \keywords{Nominal Isabelle, variable convention, theorem provers, formal reasoning, lambda-calculus} |
80 \subjclass{F.3.1} |
80 \subjclass{F.3.1} |
81 |
81 |
82 \begin{abstract} |
82 \begin{abstract} |
83 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
83 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
84 prover. It provides a proving infrastructure for reasoning about |
84 prover. It provides a proving infrastructure for reasoning about |