| author | Christian Urban <christian dot urban at kcl dot ac dot uk> | 
| Wed, 28 May 2014 12:41:09 +0100 | |
| changeset 556 | 3c214b215f7e | 
| parent 553 | c53d74b34123 | 
| child 562 | daf404920ab9 | 
| permissions | -rw-r--r-- | 
| 537 | 1 | session "Session" in "ProgTutorial" = HOL + | 
| 2 | theories [document = false] | |
| 3 | "Base" | |
| 4 | "Package/Simple_Inductive_Package" | |
| 5 | "~~/src/HOL/Number_Theory/Primes" | |
| 542 
4b96e3c8b33e
updated the CallML section with the help from Florian
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
537diff
changeset | 6 | "~~/src/HOL/Library/Code_Target_Numeral" | 
| 
4b96e3c8b33e
updated the CallML section with the help from Florian
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
537diff
changeset | 7 | "~~/src/HOL/Library/Code_Abstract_Nat" | 
| 537 | 8 | theories [quick_and_dirty, document = false] | 
| 9 | "Intro" | |
| 10 | "First_Steps" | |
| 11 | "Essential" | |
| 12 | "Advanced" | |
| 13 | "Parsing" | |
| 14 | "Tactical" | |
| 15 | "Package/Ind_Intro" | |
| 16 | "Package/Ind_Prelims" | |
| 17 | "Package/Ind_Interface" | |
| 18 | "Package/Ind_General_Scheme" | |
| 19 | "Package/Ind_Code" | |
| 20 | "Package/Ind_Extensions" | |
| 21 | "Appendix" | |
| 22 | "Recipes/Antiquotes" | |
| 23 | "Recipes/TimeLimit" | |
| 24 | "Recipes/Timing" | |
| 25 | "Recipes/ExternalSolver" | |
| 26 | "Recipes/Oracle" | |
| 27 | "Recipes/Sat" | |
| 28 | "Recipes/USTypes" | |
| 29 | "Solutions" | |
| 536 | 30 | |
| 31 | session "Cookbook" in "ProgTutorial" = HOL + | |
| 537 | 32 | options [document = pdf, browser_info = false, document_output = ".."] | 
| 536 | 33 | theories [document = false] | 
| 34 | "Base" | |
| 35 | "Package/Simple_Inductive_Package" | |
| 36 | "~~/src/HOL/Number_Theory/Primes" | |
| 542 
4b96e3c8b33e
updated the CallML section with the help from Florian
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
537diff
changeset | 37 | "~~/src/HOL/Library/Code_Target_Numeral" | 
| 
4b96e3c8b33e
updated the CallML section with the help from Florian
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
537diff
changeset | 38 | "~~/src/HOL/Library/Code_Abstract_Nat" | 
| 536 | 39 | theories [quick_and_dirty, document = true] | 
| 40 | "Intro" | |
| 41 | "First_Steps" | |
| 42 | "Essential" | |
| 43 | "Advanced" | |
| 44 | "Parsing" | |
| 45 | "Tactical" | |
| 46 | "Package/Ind_Intro" | |
| 47 | "Package/Ind_Prelims" | |
| 48 | "Package/Ind_Interface" | |
| 49 | "Package/Ind_General_Scheme" | |
| 50 | "Package/Ind_Code" | |
| 51 | "Package/Ind_Extensions" | |
| 52 | "Appendix" | |
| 53 | "Recipes/Antiquotes" | |
| 54 | "Recipes/TimeLimit" | |
| 55 | "Recipes/Timing" | |
| 56 | "Recipes/ExternalSolver" | |
| 57 | "Recipes/Oracle" | |
| 58 | "Recipes/Sat" | |
| 59 | "Recipes/USTypes" | |
| 60 | "Solutions" | |
| 556 
3c214b215f7e
some small updates for Isabelle and corrections in the Parsing chapter
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
553diff
changeset | 61 | document_files | 
| 
3c214b215f7e
some small updates for Isabelle and corrections in the Parsing chapter
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
553diff
changeset | 62 | "root.bib" | 
| 
3c214b215f7e
some small updates for Isabelle and corrections in the Parsing chapter
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
553diff
changeset | 63 | "root.tex" | 
| 
3c214b215f7e
some small updates for Isabelle and corrections in the Parsing chapter
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
553diff
changeset | 64 | "build" | 
| 536 | 65 | |
| 537 | 66 |