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
|
2440
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
4 |
["Ex/Classical",
|
0a36825b16c1
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
5 |
"Ex/CoreHaskell",
|
2482
|
6 |
"Ex/Datatypes",
|
2454
|
7 |
"Ex/Ex1",
|
1773
|
8 |
"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
|
9 |
"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
|
10 |
"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
|
11 |
"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
|
12 |
"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
|
13 |
"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
|
14 |
"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
|
15 |
"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
|
16 |
"Ex/LetRec2",
|
2454
|
17 |
"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
|
18 |
"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
|
19 |
"Ex/SingleLet",
|
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/TypeSchemes",
|
2494
|
21 |
"Ex/TypeVarsTest",
|
|
22 |
"Ex/Foo1"
|
1604
|
23 |
];
|