| author | Christian Urban <urbanc@in.tum.de> |
| Sat, 06 Nov 2010 06:18:41 +0000 | |
| changeset 2556 | 8ed62410236e |
| parent 2494 | 11133eb76f61 |
| child 2568 | 8193bbaa07fe |
| permissions | -rw-r--r-- |
|
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>
parents:
2330
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 |
|
2556
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
parents:
2494
diff
changeset
|
4 |
["../Nominal-General/Atoms", |
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
parents:
2494
diff
changeset
|
5 |
"Ex/Classical", |
| 2482 | 6 |
"Ex/Datatypes", |
|
2454
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2440
diff
changeset
|
7 |
"Ex/Ex1", |
|
1773
c0eac04ae3b4
added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
1656
diff
changeset
|
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>
parents:
2454
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>
parents:
2454
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>
parents:
2330
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>
parents:
2330
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>
parents:
2330
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>
parents:
2330
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>
parents:
2330
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>
parents:
2330
diff
changeset
|
16 |
"Ex/LetRec2", |
|
2454
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2440
diff
changeset
|
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>
parents:
2330
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>
parents:
2330
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>
parents:
2330
diff
changeset
|
20 |
"Ex/TypeSchemes", |
|
2494
11133eb76f61
added Foo1 to explore a contrived example
Christian Urban <urbanc@in.tum.de>
parents:
2482
diff
changeset
|
21 |
"Ex/TypeVarsTest", |
|
2556
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
parents:
2494
diff
changeset
|
22 |
"Ex/Foo1", |
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
parents:
2494
diff
changeset
|
23 |
"Ex/Foo2", |
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
parents:
2494
diff
changeset
|
24 |
"Ex/CoreHaskell" |
|
1604
5ab97f43ec24
More modification needed for compilation
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1485
diff
changeset
|
25 |
]; |