
\documentclass{article}

\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{url}
\usepackage{bussproofs}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{definition}{Definition}[section]
\newtheorem{lemma}{Lemma}[section]

% \usepackage{exptrees}

\newcommand\comment[1]{} 

\newcommand\MD{\ensuremath{\mathcal D}}
\newcommand\MS{\ensuremath{\mathcal S}}
\newcommand\MP{\ensuremath{\mathcal P}}
\newcommand\MQ{\ensuremath{\mathcal P}}
\newcommand\MC{\ensuremath{\mathcal C}}
\newcommand\MR{\ensuremath{\mathcal R}}
\newcommand\M{\ensuremath{\mathcal M}}

\newcommand\psl{\ensuremath\MQ_{l1} \ldots \MQ_{ln}}
\newcommand\psr{\ensuremath\MQ_{r1} \ldots \MQ_{rm}}

\begin{document}

\title{Isabelle proofs of Cut-Admissibility for GTD and S4C}

\author{Jeremy E.\ Dawson}

\maketitle

\section{Introduction and Acknowledgements}
This document describes my work in Isabelle in 2014 relating to the
cut admissibility proofs for two logics described in a set of slides
entitled "Two Examples of Cut-Elimination for Non-classical Logics",
by Grigori Mints, presented at the J\"agerfest in December 2013. 

\input{gtd}
\input{s4c}

\begin{thebibliography}{10}
\bibitem{fill-csl}
\newblock 
Ranald Clouston, Jeremy Dawson, Rajeev Gor\'e \& Alwen Tiu.
\newblock Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic.
\newblock In Proc.\ CSL, 2013. DETAILS
\end{thebibliography}

\end{document}

