--- 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