|
3194
|
1 |
session Nominal2! in "Nominal" = HOL +
|
|
|
2 |
options [document = false]
|
|
|
3 |
theories
|
|
|
4 |
"Nominal2"
|
|
|
5 |
"Atoms"
|
|
|
6 |
"Eqvt"
|
|
|
7 |
|
|
|
8 |
session Tests! in "Nominal" = Nominal2 +
|
|
|
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"
|
|
|
37 |
|
|
|
38 |
(*
|
|
|
39 |
quick_and_dirty := true;
|
|
|
40 |
|
|
|
41 |
no_document use_thys
|
|
|
42 |
["Ex/Let"];
|
|
|
43 |
*)
|
|
|
44 |
|