| author | Christian Urban <urbanc@in.tum.de> |
| Tue, 28 Jun 2011 00:30:30 +0100 | |
| changeset 2912 | 3c363a5070a5 |
| parent 2734 | eee5deb35aa8 |
| child 2926 | 37c0d7953cba |
| 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", |
|
2734
eee5deb35aa8
included old test cases for perm_simp into ROOT.ML file
Christian Urban <urbanc@in.tum.de>
parents:
2646
diff
changeset
|
5 |
"Eqvt", |
|
2646
51f75d24bd73
moved Weakening up....it does not compile when put at the last position
Christian Urban <urbanc@in.tum.de>
parents:
2644
diff
changeset
|
6 |
"Ex/Weakening", |
|
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
|
7 |
"Ex/Classical", |
| 2482 | 8 |
"Ex/Datatypes", |
|
2454
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2440
diff
changeset
|
9 |
"Ex/Ex1", |
|
1773
c0eac04ae3b4
added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
1656
diff
changeset
|
10 |
"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
|
11 |
"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
|
12 |
"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
|
13 |
"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
|
14 |
"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
|
15 |
"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
|
16 |
"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
|
17 |
"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
|
18 |
"Ex/LetRec2", |
|
2454
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2440
diff
changeset
|
19 |
"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
|
20 |
"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
|
21 |
"Ex/SingleLet", |
|
2570
1c77e15c4259
added a test for the various shallow binders
Christian Urban <urbanc@in.tum.de>
parents:
2568
diff
changeset
|
22 |
"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
|
23 |
"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
|
24 |
"Ex/TypeSchemes", |
|
2494
11133eb76f61
added Foo1 to explore a contrived example
Christian Urban <urbanc@in.tum.de>
parents:
2482
diff
changeset
|
25 |
"Ex/TypeVarsTest", |
|
2626
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents:
2618
diff
changeset
|
26 |
"Ex/Foo1", |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents:
2618
diff
changeset
|
27 |
"Ex/Foo2", |
|
2618
d17fadc20507
corrected premises of strong exhausts theorems
Christian Urban <urbanc@in.tum.de>
parents:
2617
diff
changeset
|
28 |
"Ex/CoreHaskell", |
|
2646
51f75d24bd73
moved Weakening up....it does not compile when put at the last position
Christian Urban <urbanc@in.tum.de>
parents:
2644
diff
changeset
|
29 |
"Ex/CoreHaskell2" |
|
51f75d24bd73
moved Weakening up....it does not compile when put at the last position
Christian Urban <urbanc@in.tum.de>
parents:
2644
diff
changeset
|
30 |
]; |