| author | Christian Urban <christian dot urban at kcl dot ac dot uk> | 
| Tue, 08 Jul 2014 11:18:31 +0100 | |
| changeset 3238 | b2e1a7b83e05 | 
| parent 3224 | cf451e182bf0 | 
| permissions | -rw-r--r-- | 
| 3198 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 1 | session Nominal2 in "Nominal" = HOL + | 
| 3194 | 2 | options [document = false] | 
| 3 | theories | |
| 4 | "Nominal2" | |
| 5 | "Atoms" | |
| 6 | "Eqvt" | |
| 7 | ||
| 3198 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 8 | session Examples (Tests) in "Nominal" = Nominal2 + | 
| 3194 | 9 | options [document = false] | 
| 10 | theories | |
| 11 | "Ex/Weakening" | |
| 12 | "Ex/Classical" | |
| 13 | "Ex/Datatypes" | |
| 14 | "Ex/Ex1" | |
| 15 | "Ex/ExPS3" | |
| 16 | "Ex/Multi_Recs" | |
| 17 | "Ex/Multi_Recs2" | |
| 18 | "Ex/LF" | |
| 19 | "Ex/Lambda" | |
| 20 | (*"Ex/Let",*) | |
| 21 | "Ex/LetPat" | |
| 22 | "Ex/LetRec" | |
| 23 | "Ex/LetRec2" | |
| 24 | "Ex/LetFun" | |
| 25 | "Ex/Modules" | |
| 26 | "Ex/SingleLet" | |
| 27 | "Ex/Shallow" | |
| 28 | "Ex/SystemFOmega" | |
| 29 | "Ex/TypeSchemes1" | |
| 30 | "Ex/TypeSchemes2" | |
| 31 | "Ex/TypeVarsTest" | |
| 32 | "Ex/Foo1" | |
| 33 | "Ex/Foo2" | |
| 34 | "Ex/CoreHaskell" | |
| 35 | "Ex/CoreHaskell2" | |
| 36 | "Ex/Pi" | |
| 3217 
d67a6a48f1c7
added example for locales (by Tjark Weber)
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3198diff
changeset | 37 | "Ex/Local_Contexts" | 
| 3196 | 38 | theories [quick_and_dirty] | 
| 39 | "Ex/Let" | |
| 3194 | 40 | |
| 3198 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 41 | session Tutorial_Exercises (Tests) in "Tutorial" = Nominal2 + | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 42 | options [document = false, quick_and_dirty] | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 43 | theories | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 44 | "Lambda" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 45 | "Minimal" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 46 | "Tutorial1s" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 47 | "Tutorial3s" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 48 | "Tutorial4s" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 49 | "Tutorial1" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 50 | "Tutorial2" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 51 | "Tutorial2s" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 52 | "Tutorial3" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 53 | "Tutorial4" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 54 | "Tutorial5" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 55 | "Tutorial6" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 56 | |
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 57 | session CPS (Tests) in "Nominal" = Nominal2 + | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 58 | options [document = false, quick_and_dirty] | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 59 | theories | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 60 | "Ex/CPS/Lt" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 61 | "Ex/CPS/CPS1_Plotkin" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 62 | "Ex/CPS/CPS2_DanvyNielsen" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 63 | "Ex/CPS/CPS3_DanvyFilinski" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 64 | "Ex/CPS/CPS3_DanvyFilinski_FCB2" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 65 | |
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 66 | |
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 67 | session Esop in "ESOP-Paper" = Nominal2 + | 
| 3196 | 68 | theories [document = false] | 
| 69 | "~~/src/HOL/Library/LaTeXsugar" | |
| 70 | theories | |
| 71 | "Paper" | |
| 3224 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 72 | files "document/root.bib" "document/root.tex" | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 73 | |
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 74 | session Slides1 in "Slides" = Nominal2 + | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 75 | options [document = pdf, document_output= "..", document_variants = "slides1"] | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 76 | theories | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 77 | "Slides1" | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 78 | |
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 79 | session Slides2 in "Slides" = Nominal2 + | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 80 | options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides2"] | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 81 | theories | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 82 | "Slides2" | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 83 | |
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 84 | session Slides3 in "Slides" = Nominal2 + | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 85 | options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides3"] | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 86 | theories | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 87 | "Slides3" | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 88 | |
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 89 | session Slides4 in "Slides" = Nominal2 + | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 90 | options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides4"] | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 91 | theories | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 92 | "Slides4" | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 93 | |
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 94 | session Slides5 in "Slides" = Nominal2 + | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 95 | options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides5"] | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 96 | theories | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 97 | "Slides5" | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 98 | |
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 99 | session Slides9 in "Slides" = Nominal2 + | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 100 | options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides9"] | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 101 | theories | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 102 | "Slides9" | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 103 | |
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 104 | session SlidesB in "Slides" = Nominal2 + | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 105 | options [document = pdf, document_output= "..", document_variants = "slidesb"] | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 106 | theories | 
| 
cf451e182bf0
added slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
3217diff
changeset | 107 | "SlidesB" |