author | Christian Urban <urbanc@in.tum.de> |
Tue, 28 Aug 2012 16:47:26 +0100 | |
changeset 3198 | e42d281bf5ef |
parent 3196 | ca6ca6fc28af |
child 3208 | da575186d492 |
child 3217 | d67a6a48f1c7 |
permissions | -rw-r--r-- |
3198
e42d281bf5ef
added a nefangled ROOT file
Christian Urban <urbanc@in.tum.de>
parents:
3196
diff
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:
3196
diff
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:
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 | 67 |
theories [document = false] |
68 |
"~~/src/HOL/Library/LaTeXsugar" |
|
69 |
theories |
|
70 |
"Paper" |
|
71 |
files "document/root.bib" "document/root.tex" |