ROOT
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Sat, 19 Mar 2016 21:06:48 +0000
branchNominal2-Isabelle2016
changeset 3243 c4f31f1564b7
parent 3224 cf451e182bf0
permissions -rw-r--r--
updated to Isabelle 2016

session Nominal2 in "Nominal" = HOL +
  options [document = false]
  theories
    "Nominal2"
    "Atoms"
    "Eqvt"

session Examples (Tests) in "Nominal" = Nominal2 +
  options [document = false]
  theories
    "Ex/Weakening"
    "Ex/Classical"
    "Ex/Datatypes"
    "Ex/Ex1"
    "Ex/ExPS3"
    "Ex/Multi_Recs"
    "Ex/Multi_Recs2"
    "Ex/LF"
    "Ex/Lambda"
    (*"Ex/Let",*)
    "Ex/LetPat"
    "Ex/LetRec"
    "Ex/LetRec2"
    "Ex/LetFun"
    "Ex/Modules"
    "Ex/SingleLet"
    "Ex/Shallow"
    "Ex/SystemFOmega"
    "Ex/TypeSchemes1"
    "Ex/TypeSchemes2"
    "Ex/TypeVarsTest"
    "Ex/Foo1"
    "Ex/Foo2"
    "Ex/CoreHaskell"
    "Ex/CoreHaskell2"
    "Ex/Pi"
    "Ex/Local_Contexts"
  theories [quick_and_dirty]
    "Ex/Let"

session Tutorial_Exercises (Tests) in "Tutorial" = Nominal2 +
  options [document = false, quick_and_dirty]
  theories
    "Lambda"
    "Minimal"
    "Tutorial1s"
    "Tutorial3s"
    "Tutorial4s"
    "Tutorial1"
    "Tutorial2"
    "Tutorial2s"
    "Tutorial3"
    "Tutorial4"
    "Tutorial5"
    "Tutorial6" 

session CPS (Tests) in "Nominal" = Nominal2 +
  options [document = false, quick_and_dirty]
  theories
    "Ex/CPS/Lt"
    "Ex/CPS/CPS1_Plotkin"
    "Ex/CPS/CPS2_DanvyNielsen"
    "Ex/CPS/CPS3_DanvyFilinski"	
    "Ex/CPS/CPS3_DanvyFilinski_FCB2"


session Esop in "ESOP-Paper" = Nominal2 +
   theories [document = false]
     "~~/src/HOL/Library/LaTeXsugar"
   theories 
     "Paper"
   files "document/root.bib" "document/root.tex"

session Slides1 in "Slides" = Nominal2 +
  options [document = pdf, document_output= "..", document_variants = "slides1"]
  theories
    "Slides1"

session Slides2 in "Slides" = Nominal2 +
  options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides2"]
  theories
    "Slides2"

session Slides3 in "Slides" = Nominal2 +
  options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides3"]
  theories
    "Slides3"

session Slides4 in "Slides" = Nominal2 +
  options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides4"]
  theories
    "Slides4"

session Slides5 in "Slides" = Nominal2 +
  options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides5"]
  theories
    "Slides5"

session Slides9 in "Slides" = Nominal2 +
  options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides9"]
  theories
    "Slides9"

session SlidesB in "Slides" = Nominal2 +
  options [document = pdf, document_output= "..", document_variants = "slidesb"]
  theories
    "SlidesB"