diff --git a/thys/Saturation_Framework_Extensions/document/root.tex b/thys/Saturation_Framework_Extensions/document/root.tex
--- a/thys/Saturation_Framework_Extensions/document/root.tex
+++ b/thys/Saturation_Framework_Extensions/document/root.tex
@@ -1,103 +1,103 @@
 %Some LaTeX checking: no bad pratices
 %\RequirePackage[l2tabu, orthodox]{nag}
 %\RequirePackage[all,error]{onlyamsmath}
 \RequirePackage{fixltx2e}
 
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 
 % further packages required for unusual symbols (see also
 % isabellesym.sty), use only when needed
 
 % lualatex
 %\usepackage{spelling}
 \usepackage{fullpage}
 \usepackage{graphicx}
 \usepackage{comment}
 
 
 \usepackage{mdframed}
 %% Saisie en UTF-8
 \usepackage[utf8]{inputenc}
 \usepackage[T1]{fontenc}
 \usepackage{lmodern}
 \usepackage{subcaption}
 
 %% Pour composer des mathématiques
 \usepackage{amsmath,amssymb, amsthm}
 \usepackage{nicefrac}
 \usepackage{tikz}
 \usetikzlibrary{decorations, arrows, shapes, automata, mindmap, trees}
   %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
   %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
   %\<triangleq>, \<yen>, \<lozenge>
 
 %\usepackage{eurosym}
   %for \<euro>
 
 \usepackage[only,bigsqcap]{stmaryrd}
   %for \<Sqinter>
 \usepackage{wasysym}
 
 %\usepackage{eufrak}
   %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
 
 %\usepackage{textcomp}
   %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
   %\<currency>
 
 \usepackage[english]{babel}
 % this should be the last package used
 \usepackage{pdfsetup}
 
 % urls in roman style, theory text in math-similar italics
 \urlstyle{rm}
 \isabellestyle{it}
 
 \hyphenation{Schlicht-krull}
 
 \begin{document}
 
 \title{Extensions to the Comprehensive Framework for Saturation Theorem Proving}
 \author{Jasmin Blanchette \and Sophie Tourret}
 \maketitle
 
 \begin{abstract}
 \noindent
-This Isabelle/HOL formalization extends the \emph{Archive of Formal Proofs}
-entry \verb|Saturation_Framework| with the following contributions:
+This Isabelle/HOL formalization extends the \verb|Saturation_Framework| entry of
+the \emph{Archive of Formal Proofs} with the following contributions:
 
 \begin{itemize}
 \item an application of the framework to prove Bachmair and Ganzinger's
   resolution prover \textsf{RP} refutationally complete, which was formalized
-  in a more ad hoc fashion by Schlichtkrull et al.\ in the
-  \emph{Archive of Formal Proofs} entry \verb|Ordered_Resultion_Prover|;
+  in a more ad hoc fashion by Schlichtkrull et al.\ in the \emph{AFP} entry
+  \verb|Ordered_Resultion_Prover|;
 
 \item generalizations of various basic concepts formalized by Schlichtkrull et
   al., which were needed to verify \textsf{RP} and could be useful to formalize
   other calculi, such as superposition;
 
 \item alternative proofs of fairness (and hence saturation and ultimately
-  refutational completeness) for the given clause procedures \textsf{GC} and
-  \textsf{LGC}, based on invariance.
+  refutational completeness) for the eager and lazy given clause procedures
+  (\textsf{GC} and \textsf{LGC}) based on invariance.
 \end{itemize}
 \end{abstract}
 
 \tableofcontents
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
 % generated text of all theories
 \input{session}
 
 % optional bibliography
 %\bibliographystyle{abbrv}
 %\bibliography{root}
 
 \end{document}
 
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
 %%% End: