\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\usepackage{amsmath,amssymb}

%this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

\begin{document}

\title{Banach-Steinhaus theorem\thanks{Supported by the ERC consolidator grant CerQuS (819317), the PRG team grant “Secure Quantum Technology” (PRG946) from the Estonian Research Council, and the Estonian Centre of Exellence in IT (EXCITE) funded by ERDF.}}
\author{Dominique Unruh \and Jos\'e Manuel Rodr\'iguez Caballero}
\maketitle

\begin{abstract}
We formalize in Isabelle/HOL a result \cite{Weisstein_UBP} due to S. Banach and H. Steinhaus \cite{banach1927principe} known as Banach-Steinhaus theorem or Uniform boundedness principle: a pointwise-bounded family of continuous linear operators from a Banach space to a normed space is uniformly bounded. Our approach is an adaptation to Isabelle/HOL of a proof due to A. Sokal \cite{sokal2011really}.
\end{abstract}

\tableofcontents

\input{session}


\bibliographystyle{abbrv}
\bibliography{root}

\end{document}
