ROOT
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Tue, 19 Feb 2013 05:38:46 +0000
branchNominal2-Isabelle2013
changeset 3206 fb201e383f1b
parent 3198 e42d281bf5ef
child 3208 da575186d492
child 3217 d67a6a48f1c7
permissions -rw-r--r--
added Nominal2-Isabelle 2013 Branch
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3198
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
     1
session Nominal2 in "Nominal" = HOL +
3194
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
  options [document = false]
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
  theories
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
    "Nominal2"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
    "Atoms"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
    "Eqvt"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
3198
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
     8
session Examples (Tests) in "Nominal" = Nominal2 +
3194
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
  options [document = false]
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
  theories
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
    "Ex/Weakening"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
    "Ex/Classical"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
    "Ex/Datatypes"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
    "Ex/Ex1"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
    "Ex/ExPS3"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
    "Ex/Multi_Recs"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
    "Ex/Multi_Recs2"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
    "Ex/LF"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
    "Ex/Lambda"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
    (*"Ex/Let",*)
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
    "Ex/LetPat"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
    "Ex/LetRec"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
    "Ex/LetRec2"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
    "Ex/LetFun"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
    "Ex/Modules"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
    "Ex/SingleLet"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
    "Ex/Shallow"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
    "Ex/SystemFOmega"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
    "Ex/TypeSchemes1"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
    "Ex/TypeSchemes2"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
    "Ex/TypeVarsTest"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
    "Ex/Foo1"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
    "Ex/Foo2"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
    "Ex/CoreHaskell"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    35
    "Ex/CoreHaskell2"
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
    "Ex/Pi"
3196
Christian Urban <urbanc@in.tum.de>
parents: 3194
diff changeset
    37
  theories [quick_and_dirty]
Christian Urban <urbanc@in.tum.de>
parents: 3194
diff changeset
    38
    "Ex/Let"
3194
6454435d689b added new ROOT session file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    39
3198
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    40
session Tutorial_Exercises (Tests) in "Tutorial" = Nominal2 +
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    41
  options [document = false, quick_and_dirty]
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    42
  theories
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    43
    "Lambda"
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    44
    "Minimal"
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    45
    "Tutorial1s"
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    46
    "Tutorial3s"
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    47
    "Tutorial4s"
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    48
    "Tutorial1"
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    49
    "Tutorial2"
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    50
    "Tutorial2s"
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    51
    "Tutorial3"
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    52
    "Tutorial4"
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    53
    "Tutorial5"
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    54
    "Tutorial6" 
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    55
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    56
session CPS (Tests) in "Nominal" = Nominal2 +
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    57
  options [document = false, quick_and_dirty]
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    58
  theories
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    59
    "Ex/CPS/Lt"
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    60
    "Ex/CPS/CPS1_Plotkin"
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    61
    "Ex/CPS/CPS2_DanvyNielsen"
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    62
    "Ex/CPS/CPS3_DanvyFilinski"	
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    63
    "Ex/CPS/CPS3_DanvyFilinski_FCB2"
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    64
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    65
e42d281bf5ef added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents: 3196
diff changeset
    66
session Esop in "ESOP-Paper" = Nominal2 +
3196
Christian Urban <urbanc@in.tum.de>
parents: 3194
diff changeset
    67
   theories [document = false]
Christian Urban <urbanc@in.tum.de>
parents: 3194
diff changeset
    68
     "~~/src/HOL/Library/LaTeXsugar"
Christian Urban <urbanc@in.tum.de>
parents: 3194
diff changeset
    69
   theories 
Christian Urban <urbanc@in.tum.de>
parents: 3194
diff changeset
    70
     "Paper"
Christian Urban <urbanc@in.tum.de>
parents: 3194
diff changeset
    71
   files "document/root.bib" "document/root.tex"