updated
authorChristian Urban <urbanc@in.tum.de>
Mon, 17 Sep 2012 00:07:40 +0100
changeset 537 308ba2488d40
parent 536 31d06b5cada4
child 538 e9fd5eff62c1
updated
ProgTutorial/document/build
ROOT
progtutorial.pdf
--- a/ProgTutorial/document/build	Tue Aug 28 21:23:32 2012 +0100
+++ b/ProgTutorial/document/build	Mon Sep 17 00:07:40 2012 +0100
@@ -10,10 +10,12 @@
 "$ISABELLE_TOOL" version > version.tex
 
 "$ISABELLE_TOOL" latex -o "$FORMAT"
+"$ISABELLE_TOOL" latex -o "$FORMAT"
 "$ISABELLE_TOOL" latex -o bbl
 makeindex -o root.stu root.str
 "$ISABELLE_TOOL" latex -o "$FORMAT"
 "$ISABELLE_TOOL" latex -o "$FORMAT"
+cp root.pdf ../document.pdf
 mv root.pdf ../progtutorial.pdf
 
 
--- a/ROOT	Tue Aug 28 21:23:32 2012 +0100
+++ b/ROOT	Mon Sep 17 00:07:40 2012 +0100
@@ -1,6 +1,36 @@
+session "Session" in "ProgTutorial" = HOL +
+  theories [document = false]
+    "Base"
+    "Package/Simple_Inductive_Package"
+    "~~/src/HOL/Number_Theory/Primes" 
+    "~~/src/HOL/Library/Efficient_Nat"
+    "Helper/Command/Command"
+  theories [quick_and_dirty, document = false] 
+    "Intro"
+    "First_Steps"
+    "Essential"
+    "Advanced"
+    "Parsing"
+    "Tactical"
+    "Package/Ind_Intro"
+    "Package/Ind_Prelims"
+    "Package/Ind_Interface"
+    "Package/Ind_General_Scheme"
+    "Package/Ind_Code" 
+    "Package/Ind_Extensions"
+    "Appendix"
+    "Recipes/Antiquotes"
+    "Recipes/TimeLimit"
+    "Recipes/Timing"
+    "Recipes/CallML"
+    "Recipes/ExternalSolver"
+    "Recipes/Oracle"
+    "Recipes/Sat"
+    "Recipes/USTypes"
+    "Solutions"
 
 session "Cookbook" in "ProgTutorial" = HOL +
-options [document = pdf, browser_info = false, document_output = ".."]
+  options [document = pdf, browser_info = false, document_output = ".."]
   theories [document = false]
     "Base"
     "Package/Simple_Inductive_Package"
@@ -35,3 +65,4 @@
     "document/root.tex" 
     "document/build"
 
+
Binary file progtutorial.pdf has changed