604
|
1 |
quick_and_dirty := true;
|
|
2 |
|
|
3 |
no_document use_thys
|
1128
|
4 |
["Quotient",
|
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
5 |
"Examples/AbsRepTest",
|
628
|
6 |
"Examples/FSet",
|
685
|
7 |
"Examples/FSet2",
|
720
|
8 |
"Examples/FSet3",
|
601
|
9 |
"Examples/IntEx",
|
|
10 |
"Examples/IntEx2",
|
|
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>
diff
changeset
|
12 |
"Examples/LamEx",
|
720
|
13 |
"Examples/LarryDatatype",
|
918
|
14 |
"Examples/LarryInt",
|
|
15 |
"Examples/Terms"];
|