# HG changeset patch
# User wenzelm
# Date 1544215328 -3600
# Node ID 472af2d7835d9faf7520f37ac4537b1de340816d
# Parent  71bf7903e7feb5005abc4ebf4ac374d579371b6b
clarified session dependencies: faster build_doc/build_release;

diff -r 71bf7903e7fe -r 472af2d7835d src/Doc/Codegen/Adaptation.thy
--- a/src/Doc/Codegen/Adaptation.thy	Fri Dec 07 15:30:48 2018 +0000
+++ b/src/Doc/Codegen/Adaptation.thy	Fri Dec 07 21:42:08 2018 +0100
@@ -1,5 +1,5 @@
 theory Adaptation
-imports Codegen_Basics.Setup
+imports Setup
 begin
 
 setup %invisible \<open>Code_Target.add_derived_target ("\<SML>", [("SML", I)])
diff -r 71bf7903e7fe -r 472af2d7835d src/Doc/Codegen/Computations.thy
--- a/src/Doc/Codegen/Computations.thy	Fri Dec 07 15:30:48 2018 +0000
+++ b/src/Doc/Codegen/Computations.thy	Fri Dec 07 21:42:08 2018 +0100
@@ -1,5 +1,5 @@
 theory Computations
-  imports Codegen_Basics.Setup
+  imports Setup
     "HOL-Library.Code_Target_Int"
 begin
 
diff -r 71bf7903e7fe -r 472af2d7835d src/Doc/Codegen/Evaluation.thy
--- a/src/Doc/Codegen/Evaluation.thy	Fri Dec 07 15:30:48 2018 +0000
+++ b/src/Doc/Codegen/Evaluation.thy	Fri Dec 07 21:42:08 2018 +0100
@@ -1,5 +1,5 @@
 theory Evaluation
-imports Codegen_Basics.Setup
+imports Setup
 begin (*<*)
 
 ML \<open>
diff -r 71bf7903e7fe -r 472af2d7835d src/Doc/Codegen/Further.thy
--- a/src/Doc/Codegen/Further.thy	Fri Dec 07 15:30:48 2018 +0000
+++ b/src/Doc/Codegen/Further.thy	Fri Dec 07 21:42:08 2018 +0100
@@ -1,5 +1,5 @@
 theory Further
-imports Codegen_Basics.Setup
+imports Setup
 begin
 
 section \<open>Further issues \label{sec:further}\<close>
diff -r 71bf7903e7fe -r 472af2d7835d src/Doc/Codegen/Inductive_Predicate.thy
--- a/src/Doc/Codegen/Inductive_Predicate.thy	Fri Dec 07 15:30:48 2018 +0000
+++ b/src/Doc/Codegen/Inductive_Predicate.thy	Fri Dec 07 21:42:08 2018 +0100
@@ -1,5 +1,5 @@
 theory Inductive_Predicate
-imports Codegen_Basics.Setup
+imports Setup
 begin
 
 (*<*)
diff -r 71bf7903e7fe -r 472af2d7835d src/Doc/Codegen/Introduction.thy
--- a/src/Doc/Codegen/Introduction.thy	Fri Dec 07 15:30:48 2018 +0000
+++ b/src/Doc/Codegen/Introduction.thy	Fri Dec 07 21:42:08 2018 +0100
@@ -1,5 +1,5 @@
 theory Introduction
-imports Codegen_Basics.Setup
+imports Setup
 begin (*<*)
 
 ML \<open>
diff -r 71bf7903e7fe -r 472af2d7835d src/Doc/Codegen/Refinement.thy
--- a/src/Doc/Codegen/Refinement.thy	Fri Dec 07 15:30:48 2018 +0000
+++ b/src/Doc/Codegen/Refinement.thy	Fri Dec 07 21:42:08 2018 +0100
@@ -1,5 +1,5 @@
 theory Refinement
-imports Codegen_Basics.Setup
+imports Setup
 begin
 
 section \<open>Program and datatype refinement \label{sec:refinement}\<close>
diff -r 71bf7903e7fe -r 472af2d7835d src/Doc/ROOT
--- a/src/Doc/ROOT	Fri Dec 07 15:30:48 2018 +0000
+++ b/src/Doc/ROOT	Fri Dec 07 21:42:08 2018 +0100
@@ -16,12 +16,12 @@
     "root.tex"
     "style.sty"
 
-session Codegen_Basics (no_doc) in "Codegen" = "HOL-Library" +
-  theories
+session Codegen (doc) in "Codegen" = HOL +
+  options [document_variants = "codegen", print_mode = "no_brackets,iff"]
+  sessions
+    "HOL-Library"
+  theories [document = false]
     Setup
-
-session Codegen (doc) in "Codegen" = "Codegen_Basics" +
-  options [document_variants = "codegen", print_mode = "no_brackets,iff"]
   theories
     Introduction
     Foundations
@@ -43,11 +43,10 @@
     "root.tex"
     "style.sty"
 
-session Corec (doc) in "Corec" = "HOL-Library" +
+session Corec (doc) in "Corec" = Datatypes +
   options [document_variants = "corec"]
-  sessions
-    Datatypes
-  theories Corec
+  theories
+    Corec
   document_files (in "..")
     "prepare_document"
     "pdfsetup.sty"
@@ -60,10 +59,14 @@
     "root.tex"
     "style.sty"
 
-session Datatypes (doc) in "Datatypes" = "HOL-Library" +
+session Datatypes (doc) in "Datatypes" = HOL +
   options [document_variants = "datatypes"]
-  theories [document = false] Setup
-  theories Datatypes
+  sessions
+    "HOL-Library"
+  theories [document = false]
+    Setup
+  theories
+    Datatypes
   document_files (in "..")
     "prepare_document"
     "pdfsetup.sty"
@@ -76,9 +79,11 @@
     "root.tex"
     "style.sty"
 
-session Eisbach (doc) in "Eisbach" = "HOL-Eisbach" +
+session Eisbach (doc) in "Eisbach" = HOL +
   options [document_variants = "eisbach", quick_and_dirty,
     print_mode = "no_brackets,iff", show_question_marks = false]
+  sessions
+    "HOL-Eisbach"
   theories [document = false]
     Base
   theories
@@ -141,7 +146,7 @@
     "getting.tex"
     "root.tex"
 
-session Implementation (doc) in "Implementation" = "HOL" +
+session Implementation (doc) in "Implementation" = HOL +
   options [document_variants = "implementation", quick_and_dirty]
   theories
     Eq
@@ -169,8 +174,10 @@
     "root.tex"
     "style.sty"
 
-session Isar_Ref (doc) in "Isar_Ref" = "HOL-Library" +
+session Isar_Ref (doc) in "Isar_Ref" = HOL +
   options [document_variants = "isar-ref", quick_and_dirty, thy_output_source]
+  sessions
+    "HOL-Library"
   theories
     Preface
     Synopsis
@@ -487,9 +494,14 @@
     "typedef.pdf"
     "types0.tex"
 
-session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = "Typeclass_Hierarchy_Basics" +
+session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = HOL +
   options [document_variants = "typeclass_hierarchy"]
-  theories Typeclass_Hierarchy
+  sessions
+    "HOL-Library"
+  theories [document = false]
+    Setup
+  theories
+    Typeclass_Hierarchy
   document_files (in "..")
     "prepare_document"
     "pdfsetup.sty"
@@ -501,7 +513,3 @@
     "build"
     "root.tex"
     "style.sty"
-
-session Typeclass_Hierarchy_Basics (no_doc) in "Typeclass_Hierarchy" = "HOL-Library" +
-  theories
-    Setup
diff -r 71bf7903e7fe -r 472af2d7835d src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy
--- a/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy	Fri Dec 07 15:30:48 2018 +0000
+++ b/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy	Fri Dec 07 21:42:08 2018 +0100
@@ -1,5 +1,5 @@
 theory Typeclass_Hierarchy
-imports Typeclass_Hierarchy_Basics.Setup
+imports Setup
 begin
 
 section \<open>Introduction\<close>