| author | Christian Urban <urbanc@in.tum.de> |
| Fri, 14 May 2010 17:40:43 +0100 | |
| changeset 2136 | 2fc55508a6d0 |
| parent 1260 | 9df6144e281b |
| permissions | -rw-r--r-- |
|
604
0cf166548856
isabelle make tests all examples
Christian Urban <urbanc@in.tum.de>
parents:
601
diff
changeset
|
1 |
quick_and_dirty := true; |
|
0cf166548856
isabelle make tests all examples
Christian Urban <urbanc@in.tum.de>
parents:
601
diff
changeset
|
2 |
|
|
0cf166548856
isabelle make tests all examples
Christian Urban <urbanc@in.tum.de>
parents:
601
diff
changeset
|
3 |
no_document use_thys |
|
1128
17ca92ab4660
Main renaming + fixes for new Isabelle in IntEx2.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
918
diff
changeset
|
4 |
["Quotient", |
|
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
720
diff
changeset
|
5 |
"Examples/AbsRepTest", |
|
628
a11b9b757f89
corrected name of FSet in ROOT.ML
Christian Urban <urbanc@in.tum.de>
parents:
604
diff
changeset
|
6 |
"Examples/FSet", |
|
685
b12f0321dfb0
moved the interpretation code into Unused.thy
Christian Urban <urbanc@in.tum.de>
parents:
628
diff
changeset
|
7 |
"Examples/FSet2", |
|
720
e68f501f76d0
Merge + Added LarryInt & Fset3 to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
715
diff
changeset
|
8 |
"Examples/FSet3", |
|
601
81f40b8bde7b
added "end" to each example theory
Christian Urban <urbanc@in.tum.de>
parents:
597
diff
changeset
|
9 |
"Examples/IntEx", |
|
81f40b8bde7b
added "end" to each example theory
Christian Urban <urbanc@in.tum.de>
parents:
597
diff
changeset
|
10 |
"Examples/IntEx2", |
|
81f40b8bde7b
added "end" to each example theory
Christian Urban <urbanc@in.tum.de>
parents:
597
diff
changeset
|
11 |
"Examples/LFex", |
|
700
91b079db7380
added Larry's theory; introduced lemma equivpI; added something to the TODO about error messages
Christian Urban <urbanc@in.tum.de>
parents:
685
diff
changeset
|
12 |
"Examples/LamEx", |
|
720
e68f501f76d0
Merge + Added LarryInt & Fset3 to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
715
diff
changeset
|
13 |
"Examples/LarryDatatype", |
| 918 | 14 |
"Examples/LarryInt", |
15 |
"Examples/Terms"]; |