1261
853abc14c5c6
added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
|
2440
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
2 |
|
1261
853abc14c5c6
added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
no_document use_thys
|
2568
8193bbaa07fe
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
4 |
["Atoms",
|
2646
51f75d24bd73
moved Weakening up....it does not compile when put at the last position
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
5 |
"Ex/Weakening",
|
2556
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
6 |
"Ex/Classical",
|
2482
|
7 |
"Ex/Datatypes",
|
2454
|
8 |
"Ex/Ex1",
|
1773
|
9 |
"Ex/ExPS3",
|
2481
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
10 |
"Ex/Multi_Recs",
|
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
11 |
"Ex/Multi_Recs2",
|
2440
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
12 |
"Ex/LF",
|
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
13 |
"Ex/Lambda",
|
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
14 |
"Ex/Let",
|
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
15 |
"Ex/LetPat",
|
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
"Ex/LetRec",
|
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
17 |
"Ex/LetRec2",
|
2454
|
18 |
"Ex/LetFun",
|
2440
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
19 |
"Ex/Modules",
|
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
20 |
"Ex/SingleLet",
|
2570
|
21 |
"Ex/Shallow",
|
2581
3696659358c8
added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
22 |
"Ex/SystemFOmega",
|
2440
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
23 |
"Ex/TypeSchemes",
|
2494
|
24 |
"Ex/TypeVarsTest",
|
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
25 |
"Ex/Foo1",
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
26 |
"Ex/Foo2",
|
2618
|
27 |
"Ex/CoreHaskell",
|
2646
51f75d24bd73
moved Weakening up....it does not compile when put at the last position
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
28 |
"Ex/CoreHaskell2"
|
51f75d24bd73
moved Weakening up....it does not compile when put at the last position
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
29 |
];
|