| author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
| Mon, 11 Mar 2013 16:37:54 +0000 | |
| changeset 3212 | 0f76f481dbb5 |
| parent 3112 | e4050732ba15 |
| child 3170 | 89715c48f728 |
| child 3217 | d67a6a48f1c7 |
| 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", |
|
3045
d0ad264f8c4f
updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package
Christian Urban <urbanc@in.tum.de>
parents:
2926
diff
changeset
|
7 |
"Ex/Classical", |
|
3046
9b0324e1293b
all examples work again after quotient package has been "de-localised"
Christian Urban <urbanc@in.tum.de>
parents:
3045
diff
changeset
|
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", |
|
2926
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
parents:
2734
diff
changeset
|
15 |
(*"Ex/Let",*) |
|
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
|
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", |
|
3100
8779fb01d8b4
separated the two versions of type schemes into two files
Christian Urban <urbanc@in.tum.de>
parents:
3097
diff
changeset
|
24 |
"Ex/TypeSchemes1", |
|
8779fb01d8b4
separated the two versions of type schemes into two files
Christian Urban <urbanc@in.tum.de>
parents:
3097
diff
changeset
|
25 |
"Ex/TypeSchemes2", |
|
3046
9b0324e1293b
all examples work again after quotient package has been "de-localised"
Christian Urban <urbanc@in.tum.de>
parents:
3045
diff
changeset
|
26 |
"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
|
27 |
"Ex/Foo1", |
|
d1bdc281be2b
moved all strong_exhaust code to nominal_dt_quot; tuned examples
Christian Urban <urbanc@in.tum.de>
parents:
2618
diff
changeset
|
28 |
"Ex/Foo2", |
|
2618
d17fadc20507
corrected premises of strong exhausts theorems
Christian Urban <urbanc@in.tum.de>
parents:
2617
diff
changeset
|
29 |
"Ex/CoreHaskell", |
| 3112 | 30 |
"Ex/CoreHaskell2", |
|
3097
b27e94db1b8a
included Pi theory in tests
Christian Urban <urbanc@in.tum.de>
parents:
3075
diff
changeset
|
31 |
"Ex/Pi" |
|
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
|
32 |
]; |
|
2926
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
parents:
2734
diff
changeset
|
33 |
|
|
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
parents:
2734
diff
changeset
|
34 |
quick_and_dirty := true; |
|
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
parents:
2734
diff
changeset
|
35 |
|
|
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
parents:
2734
diff
changeset
|
36 |
no_document use_thys |
| 3075 | 37 |
["Ex/Let"]; |
|
2926
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
parents:
2734
diff
changeset
|
38 |
|
|
37c0d7953cba
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
Christian Urban <urbanc@in.tum.de>
parents:
2734
diff
changeset
|
39 |