diff -r fc3e8f79e698 -r 1f9360daf6e1 Quotient-Paper/document/root.tex --- a/Quotient-Paper/document/root.tex Fri Aug 27 02:25:40 2010 +0000 +++ b/Quotient-Paper/document/root.tex Fri Aug 27 13:57:00 2010 +0800 @@ -1,5 +1,6 @@ -%\documentclass{svjour3} -\documentclass{llncs} +\documentclass{sig-alternate} + \pdfpagewidth=8.5truein + \pdfpageheight=11truein \usepackage{times} \usepackage{isabelle} \usepackage{isabellesym} @@ -11,10 +12,14 @@ \usepackage{verbdef} \usepackage{longtable} \usepackage{mathpartir} +\newtheorem{definition}{Definition} +\newtheorem{proposition}{Proposition} +\newtheorem{lemma}{Lemma} \urlstyle{rm} \isabellestyle{it} -\renewcommand{\isastyle}{\isastyleminor} +\renewcommand{\isastyleminor}{\it}% +\renewcommand{\isastyle}{\normalsize\rm}% \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} \verbdef\singlearr|--->| @@ -34,9 +39,23 @@ \begin{document} +\conferenceinfo{SAC'11}{March 21-25, 2011, TaiChung, Taiwan.} +\CopyrightYear{2011} +\crdata{978-1-4503-0113-8/11/03} + \title{Quotients Revisited for Isabelle/HOL} -\author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} -\institute{$^*$ Technical University of Munich, Germany} +\numberofauthors{2} +\author{ +\alignauthor +Cezary Kaliszyk\\ + \affaddr{University of Tsukuba, Japan}\\ + \email{kaliszyk@score.cs.tsukuba.ac.jp} +\alignauthor +Christian Urban\\ + \affaddr{Technical University of Munich, Germany}\\ + \email{urbanc@in.tum.de} +} + \maketitle \begin{abstract} @@ -54,6 +73,10 @@ $\alpha$-quotient, terms, than over raw terms. \end{abstract} +\category{D.??}{TODO}{TODO} + +\keywords{quotients, isabelle, higher order logic} + % generated text of all theories \input{session}