# 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 \Code_Target.add_derived_target ("\", [("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 \ 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 \Further issues \label{sec:further}\ 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 \ 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 \Program and datatype refinement \label{sec:refinement}\ 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 \Introduction\