diff --git a/thys/Probabilistic_System_Zoo/BNFs/Bool_Bounded_Set.thy b/thys/Probabilistic_System_Zoo/Bool_Bounded_Set.thy
rename from thys/Probabilistic_System_Zoo/BNFs/Bool_Bounded_Set.thy
rename to thys/Probabilistic_System_Zoo/Bool_Bounded_Set.thy
diff --git a/thys/Probabilistic_System_Zoo/ROOT b/thys/Probabilistic_System_Zoo/ROOT
--- a/thys/Probabilistic_System_Zoo/ROOT
+++ b/thys/Probabilistic_System_Zoo/ROOT
@@ -1,37 +1,16 @@
 chapter AFP
 
 session "Probabilistic_System_Zoo" (AFP) = "HOL-Probability" +
-  options [timeout = 600]
+  options [timeout = 600, document_variants = "document:outline=/proof,/ML:bnfs:non_bnfs"]
   sessions
     "HOL-Eisbach"
     "HOL-Cardinals"
-  theories [document = false]
+  theories
+    Bool_Bounded_Set
+    Finitely_Bounded_Set_Counterexample
     Nonempty_Bounded_Set
-  theories
-    Probabilistic_Hierarchy
-    Vardi
+    Vardi_Counterexample
   document_files
     "root.tex"
-
-session "Probabilistic_System_Zoo-BNFs" (AFP) in BNFs = "HOL-Analysis" +
-  options [timeout = 600]
-  sessions
-    "HOL-Probability"
-    "HOL-Cardinals"
-  directories ".." (overlapping)
-  theories
-    "../Nonempty_Bounded_Set"
-    Bool_Bounded_Set
-  document_files
-    "root.tex"
-
-session "Probabilistic_System_Zoo-Non_BNFs" (AFP) in Non_BNFs = "HOL-Probability" +
-  options [timeout = 600]
-  sessions
-    "HOL-Eisbach"
-    "HOL-Cardinals"
-  directories ".." (overlapping)
-  theories
-    "../Vardi"
-  document_files
-    "root.tex"
+    "root_bnfs.tex"
+    "root_non_bnfs.tex"
diff --git a/thys/Probabilistic_System_Zoo/document/root.tex b/thys/Probabilistic_System_Zoo/document/root.tex
--- a/thys/Probabilistic_System_Zoo/document/root.tex
+++ b/thys/Probabilistic_System_Zoo/document/root.tex
@@ -1,38 +1,39 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 \usepackage[ngerman,english]{babel}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{eufrak}
 
 % 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{Probabilistic Hierarchy}
 \author{Johannes H\"olzl \and Andreas Lochbihler \and Dmitriy Traytel}
 \maketitle
 
 \tableofcontents
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
 % generated text of all theories
-\input{session}
+\input{Probabilistic_Hierarchy}
+\input{Vardi}
 
 % optional bibliography
 %\bibliographystyle{abbrv}
 %\bibliography{root}
 
 \end{document}
 
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
 %%% End:
diff --git a/thys/Probabilistic_System_Zoo/BNFs/document/root.tex b/thys/Probabilistic_System_Zoo/document/root_bnfs.tex
rename from thys/Probabilistic_System_Zoo/BNFs/document/root.tex
rename to thys/Probabilistic_System_Zoo/document/root_bnfs.tex
--- a/thys/Probabilistic_System_Zoo/BNFs/document/root.tex
+++ b/thys/Probabilistic_System_Zoo/document/root_bnfs.tex
@@ -1,38 +1,38 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 \usepackage[ngerman,english]{babel}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{eufrak}
 % 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{Types Proved Being BNFs during the\\Formalization of the Probabilistic
   Hierarchy} \author{Johannes H\"olzl \and Andreas Lochbihler \and Dmitriy
   Traytel}
 \maketitle
 
 \tableofcontents
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
 % generated text of all theories
-\input{session}
+\input{Nonempty_Bounded_Set}
 
 % optional bibliography
 %\bibliographystyle{abbrv}
 %\bibliography{root}
 
 \end{document}
 
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
 %%% End:
diff --git a/thys/Probabilistic_System_Zoo/Non_BNFs/document/root.tex b/thys/Probabilistic_System_Zoo/document/root_non_bnfs.tex
rename from thys/Probabilistic_System_Zoo/Non_BNFs/document/root.tex
rename to thys/Probabilistic_System_Zoo/document/root_non_bnfs.tex
--- a/thys/Probabilistic_System_Zoo/Non_BNFs/document/root.tex
+++ b/thys/Probabilistic_System_Zoo/document/root_non_bnfs.tex
@@ -1,38 +1,39 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 \usepackage[ngerman,english]{babel}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{eufrak}
 
 % 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{Types Disproved Being BNFs during the Formalization of the Probabilistic Hierarchy}
 \author{Johannes H\"olzl \and Andreas Lochbihler \and Dmitriy Traytel}
 \maketitle
 
 \tableofcontents
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
 % generated text of all theories
-\input{session}
+\input{Finitely_Bounded_Set_Counterexample}
+\input{Vardi_Counterexample}
 
 % optional bibliography
 %\bibliographystyle{abbrv}
 %\bibliography{root}
 
 \end{document}
 
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
 %%% End: