| author | Christian Urban <christian dot urban at kcl dot ac dot uk> | 
| Fri, 01 Mar 2013 00:49:15 +0000 | |
| changeset 543 | cd28458c2add | 
| parent 542 | 4b96e3c8b33e | 
| child 553 | c53d74b34123 | 
| 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 | "Helper/Command/Command" | 
| 9 | theories [quick_and_dirty, document = false] | |
| 10 | "Intro" | |
| 11 | "First_Steps" | |
| 12 | "Essential" | |
| 13 | "Advanced" | |
| 14 | "Parsing" | |
| 15 | "Tactical" | |
| 16 | "Package/Ind_Intro" | |
| 17 | "Package/Ind_Prelims" | |
| 18 | "Package/Ind_Interface" | |
| 19 | "Package/Ind_General_Scheme" | |
| 20 | "Package/Ind_Code" | |
| 21 | "Package/Ind_Extensions" | |
| 22 | "Appendix" | |
| 23 | "Recipes/Antiquotes" | |
| 24 | "Recipes/TimeLimit" | |
| 25 | "Recipes/Timing" | |
| 26 | "Recipes/CallML" | |
| 27 | "Recipes/ExternalSolver" | |
| 28 | "Recipes/Oracle" | |
| 29 | "Recipes/Sat" | |
| 30 | "Recipes/USTypes" | |
| 31 | "Solutions" | |
| 536 | 32 | |
| 33 | session "Cookbook" in "ProgTutorial" = HOL + | |
| 537 | 34 | options [document = pdf, browser_info = false, document_output = ".."] | 
| 536 | 35 | theories [document = false] | 
| 36 | "Base" | |
| 37 | "Package/Simple_Inductive_Package" | |
| 38 | "~~/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 | 39 | "~~/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 | 40 | "~~/src/HOL/Library/Code_Abstract_Nat" | 
| 536 | 41 | "Helper/Command/Command" | 
| 42 | theories [quick_and_dirty, document = true] | |
| 43 | "Intro" | |
| 44 | "First_Steps" | |
| 45 | "Essential" | |
| 46 | "Advanced" | |
| 47 | "Parsing" | |
| 48 | "Tactical" | |
| 49 | "Package/Ind_Intro" | |
| 50 | "Package/Ind_Prelims" | |
| 51 | "Package/Ind_Interface" | |
| 52 | "Package/Ind_General_Scheme" | |
| 53 | "Package/Ind_Code" | |
| 54 | "Package/Ind_Extensions" | |
| 55 | "Appendix" | |
| 56 | "Recipes/Antiquotes" | |
| 57 | "Recipes/TimeLimit" | |
| 58 | "Recipes/Timing" | |
| 59 | "Recipes/CallML" | |
| 60 | "Recipes/ExternalSolver" | |
| 61 | "Recipes/Oracle" | |
| 62 | "Recipes/Sat" | |
| 63 | "Recipes/USTypes" | |
| 64 | "Solutions" | |
| 65 | files | |
| 66 | "document/root.bib" | |
| 67 | "document/root.tex" | |
| 68 | "document/build" | |
| 69 | ||
| 537 | 70 |