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