45 \newcommand{\AND}{\;\mathtt{and}\;} |
45 \newcommand{\AND}{\;\mathtt{and}\;} |
46 \newcommand{\fv}{\mathit{fv}} |
46 \newcommand{\fv}{\mathit{fv}} |
47 |
47 |
48 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}} |
48 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}} |
49 %----------------- theorem definitions ---------- |
49 %----------------- theorem definitions ---------- |
50 \theoremstyle{plain} |
50 %%\theoremstyle{plain} |
51 \newtheorem{thm}{Theorem}[section] |
51 %%\spnewtheorem{thm}[section]{Theorem} |
52 \newtheorem{property}[thm]{Property} |
52 %%\newtheorem{property}[thm]{Property} |
53 \newtheorem{lemma}[thm]{Lemma} |
53 %%\newtheorem{lemma}[thm]{Lemma} |
54 \newtheorem{defn}[thm]{Definition} |
54 %%\spnewtheorem{defn}[theorem]{Definition} |
55 \newtheorem{exmple}[thm]{Example} |
55 %%\spnewtheorem{exmple}[theorem]{Example} |
56 |
56 |
57 %-------------------- environment definitions ----------------- |
57 %-------------------- environment definitions ----------------- |
58 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{} |
58 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{} |
59 |
59 |
60 |
60 |
61 \begin{document} |
61 \begin{document} |
62 |
62 |
63 \title{\LARGE\bf General Bindings and Alpha-Equivalence in Nominal Isabelle} |
63 \title{General Bindings and Alpha-Equivalence in Nominal Isabelle} |
64 \authorinfo{Christian Urban and Cezary Kaliszyk} |
64 \author{Christian Urban and Cezary Kaliszyk} |
65 {TU Munich, Germany} |
65 \institute{TU Munich, Germany} |
66 {\{urbanc, kaliszyk\}@in.tum.de} |
66 %%%{\{urbanc, kaliszyk\}@in.tum.de} |
67 \maketitle |
67 \maketitle |
68 |
68 |
69 \begin{abstract} |
69 \begin{abstract} |
70 Nominal Isabelle is a definitional extension of the popular Isabelle/HOL |
70 Nominal Isabelle is a definitional extension of the popular Isabelle/HOL |
71 theorem |
71 theorem |
82 convention already built in. |
82 convention already built in. |
83 \end{abstract} |
83 \end{abstract} |
84 |
84 |
85 %\category{F.4.1}{subcategory}{third-level} |
85 %\category{F.4.1}{subcategory}{third-level} |
86 |
86 |
87 \terms |
87 %\terms |
88 formal reasoning, programming language calculi |
88 %formal reasoning, programming language calculi |
89 |
89 |
90 \keywords |
90 %\keywords |
91 nominal logic work, variable convention |
91 %nominal logic work, variable convention |
92 |
92 |
93 |
93 |
94 \input{session} |
94 \input{session} |
95 |
95 |
96 \bibliographystyle{plain} |
96 \bibliographystyle{plain} |