--- a/src/HOL/ROOT Thu Sep 17 09:57:30 2020 +0000 +++ b/src/HOL/ROOT Thu Sep 17 09:57:31 2020 +0000 @@ -898,7 +898,6 @@ Word More_Word Word_Examples - Conversions document_files "root.bib" "root.tex" session "HOL-Statespace" in Statespace = HOL +