equal
deleted
inserted
replaced
1 \documentclass{llncs} |
1 \documentclass{svjour3} |
2 \usepackage{times} |
2 \usepackage{times} |
3 \usepackage{isabelle} |
3 \usepackage{isabelle} |
4 \usepackage{isabellesym} |
4 \usepackage{isabellesym} |
5 \usepackage{amsmath} |
5 \usepackage{amsmath} |
6 \usepackage{amssymb} |
6 \usepackage{amssymb} |
23 |
23 |
24 |
24 |
25 \begin{document} |
25 \begin{document} |
26 |
26 |
27 \title{Implementing the Nominal Logic Work in Isabelle/HOL} |
27 \title{Implementing the Nominal Logic Work in Isabelle/HOL} |
28 \author{Brian Huffman\inst{1} and Christian Urban\inst{2}} |
28 \author{Christian Urban \and Brian Huffman} |
29 \institute{Portland State University \and Technical University of Munich} |
29 \institute{C.~Urban \at Technical University of Munich |
|
30 \and B.~Huffman \at Portland State University} |
|
31 \date{Received: date / Accepted: date} |
|
32 |
30 \maketitle |
33 \maketitle |
31 |
34 |
32 \begin{abstract} |
35 \begin{abstract} |
33 Pitts et al introduced a beautiful theory about names and binding based on the |
36 Pitts et al introduced a beautiful theory about names and binding based on the |
34 notions of atoms, permutations and support. The engineering challenge is to |
37 notions of atoms, permutations and support. The engineering challenge is to |