--- a/ROOT Fri Jun 03 15:15:17 2016 +0100
+++ b/ROOT Tue May 14 11:10:53 2019 +0200
@@ -1,22 +1,19 @@
-session "Session" in "ProgTutorial" = HOL +
+session "Cookbook" in "ProgTutorial" = HOL +
+ options [document = pdf, browser_info = false, document_output = ".."]
theories [document = false]
"Base"
"Package/Simple_Inductive_Package"
- "~~/src/HOL/Number_Theory/Primes"
- "~~/src/HOL/Library/Code_Target_Numeral"
- "~~/src/HOL/Library/Code_Abstract_Nat"
- theories [quick_and_dirty, document = false]
+ theories [quick_and_dirty, document = true]
"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_Code"
"Package/Ind_Extensions"
"Appendix"
"Recipes/Antiquotes"
@@ -27,40 +24,9 @@
"Recipes/Sat"
"Recipes/USTypes"
"Solutions"
-
-session "Cookbook" in "ProgTutorial" = HOL +
- options [document = pdf, browser_info = false, document_output = ".."]
- theories [document = false]
- "Base"
- "Package/Simple_Inductive_Package"
- "~~/src/HOL/Number_Theory/Primes"
- "~~/src/HOL/Library/Code_Target_Numeral"
- "~~/src/HOL/Library/Code_Abstract_Nat"
- theories [quick_and_dirty, document = true]
- "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/ExternalSolver"
- "Recipes/Oracle"
- "Recipes/Sat"
- "Recipes/USTypes"
- "Solutions"
- document_files
- "root.bib"
- "root.tex"
- "build"
+ document_files
+ "root.bib"
+ "root.tex"
+ "tutorial-logo.jpg"