| author | Christian Urban <christian dot urban at kcl dot ac dot uk> | 
| Tue, 19 Feb 2013 05:38:46 +0000 | |
| branch | Nominal2-Isabelle2013 | 
| changeset 3206 | fb201e383f1b | 
| parent 3198 | e42d281bf5ef | 
| child 3208 | da575186d492 | 
| child 3217 | d67a6a48f1c7 | 
| 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" | |
| 3196 | 37 | theories [quick_and_dirty] | 
| 38 | "Ex/Let" | |
| 3194 | 39 | |
| 3198 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 40 | session Tutorial_Exercises (Tests) in "Tutorial" = Nominal2 + | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 41 | options [document = false, quick_and_dirty] | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 42 | theories | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 43 | "Lambda" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 44 | "Minimal" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 45 | "Tutorial1s" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 46 | "Tutorial3s" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 47 | "Tutorial4s" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 48 | "Tutorial1" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 49 | "Tutorial2" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 50 | "Tutorial2s" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 51 | "Tutorial3" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 52 | "Tutorial4" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 53 | "Tutorial5" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 54 | "Tutorial6" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 55 | |
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 56 | session CPS (Tests) in "Nominal" = Nominal2 + | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 57 | options [document = false, quick_and_dirty] | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 58 | theories | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 59 | "Ex/CPS/Lt" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 60 | "Ex/CPS/CPS1_Plotkin" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 61 | "Ex/CPS/CPS2_DanvyNielsen" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 62 | "Ex/CPS/CPS3_DanvyFilinski" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 63 | "Ex/CPS/CPS3_DanvyFilinski_FCB2" | 
| 
e42d281bf5ef
added a nefangled ROOT file
 Christian Urban <urbanc@in.tum.de> parents: 
3196diff
changeset | 64 | |
| 
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 | session Esop in "ESOP-Paper" = Nominal2 + | 
| 3196 | 67 | theories [document = false] | 
| 68 | "~~/src/HOL/Library/LaTeXsugar" | |
| 69 | theories | |
| 70 | "Paper" | |
| 71 | files "document/root.bib" "document/root.tex" |