--- a/src/Doc/Codegen/Evaluation.thy Thu Jan 15 13:39:41 2015 +0100
+++ b/src/Doc/Codegen/Evaluation.thy Thu Jan 15 13:39:41 2015 +0100
@@ -1,6 +1,10 @@
theory Evaluation
imports Setup
-begin
+begin (*<*)
+
+ML \<open>
+ Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples"))
+\<close> (*>*)
section \<open>Evaluation \label{sec:evaluation}\<close>
--- a/src/Doc/Codegen/Further.thy Thu Jan 15 13:39:41 2015 +0100
+++ b/src/Doc/Codegen/Further.thy Thu Jan 15 13:39:41 2015 +0100
@@ -1,5 +1,5 @@
theory Further
-imports Setup "~~/src/Tools/Permanent_Interpretation"
+imports Setup
begin
section \<open>Further issues \label{sec:further}\<close>
--- a/src/Doc/Codegen/Introduction.thy Thu Jan 15 13:39:41 2015 +0100
+++ b/src/Doc/Codegen/Introduction.thy Thu Jan 15 13:39:41 2015 +0100
@@ -1,6 +1,10 @@
theory Introduction
imports Setup
-begin
+begin (*<*)
+
+ML \<open>
+ Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples"))
+\<close> (*>*)
section \<open>Introduction\<close>
--- a/src/Doc/Codegen/Setup.thy Thu Jan 15 13:39:41 2015 +0100
+++ b/src/Doc/Codegen/Setup.thy Thu Jan 15 13:39:41 2015 +0100
@@ -1,16 +1,13 @@
theory Setup
imports
Complex_Main
+ "~~/src/Tools/Permanent_Interpretation"
"~~/src/HOL/Library/Dlist"
"~~/src/HOL/Library/RBT"
"~~/src/HOL/Library/Mapping"
"~~/src/HOL/Library/IArray"
begin
-ML \<open>
- Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples"))
-\<close>
-
ML_file "../antiquote_setup.ML"
ML_file "../more_antiquote.ML"
--- a/src/Doc/ROOT Thu Jan 15 13:39:41 2015 +0100
+++ b/src/Doc/ROOT Thu Jan 15 13:39:41 2015 +0100
@@ -16,9 +16,12 @@
"root.tex"
"style.sty"
-session Codegen (doc) in "Codegen" = "HOL-Library" +
+session Codegen_Basics in "Codegen" = "HOL" +
+ theories [document = false]
+ Setup
+
+session Codegen (doc) in "Codegen" = "Codegen_Basics" +
options [document_variants = "codegen", print_mode = "no_brackets,iff"]
- theories [document = false] Setup
theories
Introduction
Foundations