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