# HG changeset patch
# User wenzelm
# Date 1512593000 -3600
# Node ID 8021ea06aad830800b2de5bd1af8ad53e3b5312a
# Parent  d1ace598c026159670b4e88853a242cb4fd225ca
just one session for bulky HOL-Analysis documents;

diff -r d1ace598c026 -r 8021ea06aad8 src/Doc/ROOT
--- a/src/Doc/ROOT	Wed Dec 06 21:30:26 2017 +0100
+++ b/src/Doc/ROOT	Wed Dec 06 21:43:20 2017 +0100
@@ -1,19 +1,5 @@
 chapter Doc
 
-session Analysis (doc) in "../HOL/Analysis" = HOL +
-  options [document_variants = "analysis",
-    (*skip_proofs = true,*) quick_and_dirty,
-    document = pdf, document_output = "output",
-    document_variants = "document=-proof,-ML,+important,-unimportant",
-    document_tags = "unimportant"]
-  sessions
-    "HOL-Library"
-    "HOL-Computational_Algebra"
-  theories
-    Analysis
-  document_files
-    "root.tex"
-
 session Classes (doc) in "Classes" = HOL +
   options [document_variants = "classes", quick_and_dirty]
   theories [document = false] Setup
diff -r d1ace598c026 -r 8021ea06aad8 src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Dec 06 21:30:26 2017 +0100
+++ b/src/HOL/ROOT	Wed Dec 06 21:43:20 2017 +0100
@@ -56,7 +56,10 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-Analysis" (main timing) in Analysis = HOL +
+  options [document_tags = "unimportant",
+    document_variants = "document:manual=-proof,-ML,-unimportant"]
   sessions
+    "HOL-Library"
     "HOL-Computational_Algebra"
   theories
     Analysis