diff -r 422186a35be8 -r 6b021e8cb8da src/Tools/isac/Doc/Specify_Phase/document/root.tex
--- a/src/Tools/isac/Doc/Specify_Phase/document/root.tex	Thu Apr 08 13:27:27 2021 +0200
+++ b/src/Tools/isac/Doc/Specify_Phase/document/root.tex	Tue Apr 13 13:20:05 2021 +0200
@@ -1,6 +1,7 @@
-\documentclass{article}
+\documentclass{report}
 \usepackage{isabelle,isabellesym}
 \usepackage{graphicx}
+\usepackage{paralist}  % compactitem
 % this should be the last package used
 \usepackage{pdfsetup}
 
@@ -13,6 +14,9 @@
 
 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
+\def\see{$\rightarrow$}
+\newtheorem{UR}{UR}[section]
+\newtheorem{Expl}{Expl}[section]
 
 \begin{document}
 
@@ -27,10 +31,8 @@
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
-\nocite{*}  %FIXME satisfy bibtex without actual text + citations
-%\input{user-requirements.tex}  %FIXME does not quite work yet
-
 % generated text of all theories
+\input{user-requirements.tex}
 \input{Specify_Phase.tex}  %*.tex created by isabelle build
 
 % optional bibliography