--- 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)])
--- 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
--- 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>
--- 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>
--- 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
(*<*)
--- 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>
--- 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>
--- 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
--- 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>