diff -r 8bb064045b4e -r e51c9a67a68d thys/ROOT
--- a/thys/ROOT	Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/ROOT	Sun Oct 10 00:56:47 2021 +0100
@@ -1,39 +1,23 @@
-session "Lex" = HOL +
-  theories [document = false]
-        "Spec"
-	(*"SpecExt"*)
-        "Lexer"
-        (*"LexerExt"*)
-        "Simplifying"
-        "Sulzmann" 
-        "Positions"
-	(*"PositionsExt"*)
-        "Exercises"
 
-session Paper in "Paper" = Lex +
-  options [document = pdf, document_output = "..", document_variants="paper"]
-  theories 
-    "~~/src/HOL/Library/LaTeXsugar"
-    "Paper"
-  document_files
-    "root.bib"
-    "root.tex" 
 
 
-session Journal in "Journal" = HOL +
-  options [document = pdf, document_output = "..", document_variants="journal"]
+session Journal in Journal = "HOL" +
+  options [document_output = "..", document_variants="journal"]
+  sessions
+    "HOL-Library"
+  directories
+     ".." 
   theories [document = false]
-     "~~/src/HOL/Library/LaTeXsugar"
-     "~~/src/HOL/Library/Sublist"
+     "HOL-Library.LaTeXsugar"
+     "HOL-Library.Sublist"
      "../Spec"
+     "../Lexer"
      "../RegLangs"
-     "../Lexer"
      "../Simplifying"
      "../Sulzmann" 
-     "../Positions"
+     "../Positions"   
   theories [document = true] 
-    "Paper"
-    "PaperExt"
+     "Paper"
   document_files
-    "root.bib"
-    "root.tex" 
+     "root.bib"
+     "root.tex" 
\ No newline at end of file