# HG changeset patch
# User haftmann
# Date 1421325581 -3600
# Node ID 065f349852e667c7e09bb992ff396f071f984ade
# Parent  056945909f60d6fc502630fad9465b5c98ceda29
separate image for prerequisites of codegen tutorial

diff -r 056945909f60 -r 065f349852e6 src/Doc/Codegen/Evaluation.thy
--- 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>
 
diff -r 056945909f60 -r 065f349852e6 src/Doc/Codegen/Further.thy
--- 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>
diff -r 056945909f60 -r 065f349852e6 src/Doc/Codegen/Introduction.thy
--- 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>
 
diff -r 056945909f60 -r 065f349852e6 src/Doc/Codegen/Setup.thy
--- 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"
 
diff -r 056945909f60 -r 065f349852e6 src/Doc/ROOT
--- 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