| author | Christian Urban <urbanc@in.tum.de> |
| Sat, 27 Nov 2010 22:55:29 +0000 | |
| changeset 2586 | 3ebc7ecfb0dd |
| parent 2581 | 3696659358c8 |
| child 2617 | e44551d067e6 |
| 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 |
|
2568
8193bbaa07fe
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
parents:
2556
diff
changeset
|
4 |
["Atoms", |
|
8193bbaa07fe
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
parents:
2556
diff
changeset
|
5 |
"Nominal2_Abs", |
|
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
|
6 |
"Ex/Classical", |
| 2482 | 7 |
"Ex/Datatypes", |
|
2454
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2440
diff
changeset
|
8 |
"Ex/Ex1", |
|
1773
c0eac04ae3b4
added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
1656
diff
changeset
|
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>
parents:
2454
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>
parents:
2454
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>
parents:
2330
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>
parents:
2330
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>
parents:
2330
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>
parents:
2330
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>
parents:
2330
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>
parents:
2330
diff
changeset
|
17 |
"Ex/LetRec2", |
|
2454
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2440
diff
changeset
|
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>
parents:
2330
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>
parents:
2330
diff
changeset
|
20 |
"Ex/SingleLet", |
|
2570
1c77e15c4259
added a test for the various shallow binders
Christian Urban <urbanc@in.tum.de>
parents:
2568
diff
changeset
|
21 |
"Ex/Shallow", |
|
2581
3696659358c8
added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
2570
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>
parents:
2330
diff
changeset
|
23 |
"Ex/TypeSchemes", |
|
2494
11133eb76f61
added Foo1 to explore a contrived example
Christian Urban <urbanc@in.tum.de>
parents:
2482
diff
changeset
|
24 |
"Ex/TypeVarsTest", |
|
2586
3ebc7ecfb0dd
disabled the Foo examples, because of heavy work
Christian Urban <urbanc@in.tum.de>
parents:
2581
diff
changeset
|
25 |
(*"Ex/Foo1", |
|
3ebc7ecfb0dd
disabled the Foo examples, because of heavy work
Christian Urban <urbanc@in.tum.de>
parents:
2581
diff
changeset
|
26 |
"Ex/Foo2",*) |
|
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
|
27 |
"Ex/CoreHaskell" |
|
1604
5ab97f43ec24
More modification needed for compilation
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1485
diff
changeset
|
28 |
]; |