equal
deleted
inserted
replaced
|
1 theory Find_Unused_Assms_Examples |
|
2 imports Complex_Main |
|
3 begin |
|
4 |
|
5 section {* Arithmetics *} |
|
6 |
|
7 declare [[quickcheck_finite_types = false]] |
|
8 |
|
9 find_unused_assms Divides |
|
10 find_unused_assms GCD |
|
11 find_unused_assms Real |
|
12 |
|
13 section {* Set Theory *} |
|
14 |
|
15 declare [[quickcheck_finite_types = true]] |
|
16 |
|
17 find_unused_assms Fun |
|
18 find_unused_assms Relation |
|
19 find_unused_assms Set |
|
20 find_unused_assms Wellfounded |
|
21 |
|
22 section {* Datatypes *} |
|
23 |
|
24 find_unused_assms List |
|
25 find_unused_assms Map |
|
26 |
|
27 end |