diff --git a/thys/Gale_Shapley/document/root.tex b/thys/Gale_Shapley/document/root.tex
--- a/thys/Gale_Shapley/document/root.tex
+++ b/thys/Gale_Shapley/document/root.tex
@@ -1,59 +1,59 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{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{Gale-Shapley Algorithm}
-\author{Tobias Nipkow}
+\author{Tobias Nipkow\\Department of Informatics\\Technical University of Munich}
 \maketitle
 
 \begin{abstract}
   This is a stepwise refinement and proof of the Gale-Shapley stable
   matching (or marriage) algorithm down to executable code. Both a
   purely functional implementation based on lists and a
   functional implementation based on efficient arrays (provided
   by the Collections entry in the AFP) are developed.  The latter
   implementation runs in time $O(n^2)$ where $n$ is the cardinality of
   the two sets to be matched.
 \end{abstract}
 
 \section{Introduction}
 
 The Gale-Shapley algorithm \cite{GaleS62,GusfieldI89} for stable
 matchings (or marriages) matches two sets of the same cardinality $n$,
 where each element has a complete list of preferences (a linear order)
 of the elements of the other set.
 
 The refinement process is carried out largely on the level of a simple
 imperative language. In every refinement step the whole algorithm is
 stated and proved. Most of the proof is abstrtacted into general
 lemmas that are used in multiple proofs. Except for one bigger step,
 each algorithm proof is obtained from the previous one by incremental changes.
 In the end, two executable functional algorithms are obtained:
 a purely functional one based on lists and a functional one based on a
 persistent imperative implementation of arrays (provided by the AFP entry
 Collections Framework \cite{Collections-AFP} based on \cite{Baker91}
 (see also \cite{ConchonF07})).
 The latter algorithm has linear complexity, i.e. $O(n^2)$.
 
 We prove that each of the algorithm computes a stable matching that is
 optimal for one of the two sets.
 
 \newpage
 
 % include generated text of all theories
 \input{session}
 
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}