separate image for prerequisites of codegen tutorial
authorhaftmann
Thu Jan 15 13:39:41 2015 +0100 (2015-01-15)
changeset 59378065f349852e6
parent 59377 056945909f60
child 59379 c7f6f01ede15
separate image for prerequisites of codegen tutorial
src/Doc/Codegen/Evaluation.thy
src/Doc/Codegen/Further.thy
src/Doc/Codegen/Introduction.thy
src/Doc/Codegen/Setup.thy
src/Doc/ROOT
     1.1 --- a/src/Doc/Codegen/Evaluation.thy	Thu Jan 15 13:39:41 2015 +0100
     1.2 +++ b/src/Doc/Codegen/Evaluation.thy	Thu Jan 15 13:39:41 2015 +0100
     1.3 @@ -1,6 +1,10 @@
     1.4  theory Evaluation
     1.5  imports Setup
     1.6 -begin
     1.7 +begin (*<*)
     1.8 +
     1.9 +ML \<open>
    1.10 +  Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples"))
    1.11 +\<close> (*>*)
    1.12  
    1.13  section \<open>Evaluation \label{sec:evaluation}\<close>
    1.14  
     2.1 --- a/src/Doc/Codegen/Further.thy	Thu Jan 15 13:39:41 2015 +0100
     2.2 +++ b/src/Doc/Codegen/Further.thy	Thu Jan 15 13:39:41 2015 +0100
     2.3 @@ -1,5 +1,5 @@
     2.4  theory Further
     2.5 -imports Setup "~~/src/Tools/Permanent_Interpretation"
     2.6 +imports Setup
     2.7  begin
     2.8  
     2.9  section \<open>Further issues \label{sec:further}\<close>
     3.1 --- a/src/Doc/Codegen/Introduction.thy	Thu Jan 15 13:39:41 2015 +0100
     3.2 +++ b/src/Doc/Codegen/Introduction.thy	Thu Jan 15 13:39:41 2015 +0100
     3.3 @@ -1,6 +1,10 @@
     3.4  theory Introduction
     3.5  imports Setup
     3.6 -begin
     3.7 +begin (*<*)
     3.8 +
     3.9 +ML \<open>
    3.10 +  Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples"))
    3.11 +\<close> (*>*)
    3.12  
    3.13  section \<open>Introduction\<close>
    3.14  
     4.1 --- a/src/Doc/Codegen/Setup.thy	Thu Jan 15 13:39:41 2015 +0100
     4.2 +++ b/src/Doc/Codegen/Setup.thy	Thu Jan 15 13:39:41 2015 +0100
     4.3 @@ -1,16 +1,13 @@
     4.4  theory Setup
     4.5  imports
     4.6    Complex_Main
     4.7 +  "~~/src/Tools/Permanent_Interpretation"
     4.8    "~~/src/HOL/Library/Dlist"
     4.9    "~~/src/HOL/Library/RBT"
    4.10    "~~/src/HOL/Library/Mapping"
    4.11    "~~/src/HOL/Library/IArray"
    4.12  begin
    4.13  
    4.14 -ML \<open>
    4.15 -  Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples"))
    4.16 -\<close>
    4.17 -
    4.18  ML_file "../antiquote_setup.ML"
    4.19  ML_file "../more_antiquote.ML"
    4.20  
     5.1 --- a/src/Doc/ROOT	Thu Jan 15 13:39:41 2015 +0100
     5.2 +++ b/src/Doc/ROOT	Thu Jan 15 13:39:41 2015 +0100
     5.3 @@ -16,9 +16,12 @@
     5.4      "root.tex"
     5.5      "style.sty"
     5.6  
     5.7 -session Codegen (doc) in "Codegen" = "HOL-Library" +
     5.8 +session Codegen_Basics in "Codegen" = "HOL" +
     5.9 +  theories [document = false]
    5.10 +    Setup
    5.11 +
    5.12 +session Codegen (doc) in "Codegen" = "Codegen_Basics" +
    5.13    options [document_variants = "codegen", print_mode = "no_brackets,iff"]
    5.14 -  theories [document = false] Setup
    5.15    theories
    5.16      Introduction
    5.17      Foundations