author | wenzelm |
Wed, 06 Apr 2016 23:45:19 +0200 | |
changeset 62895 | 54c2abe7e9a4 |
parent 62290 | 658276428cfc |
child 70118 | 62b875ba33e1 |
permissions | -rw-r--r-- |
46590 | 1 |
theory Find_Unused_Assms_Examples |
46673
34e26d5119ef
adding some more test invocations of find_unused_assms
bulwahn
parents:
46590
diff
changeset
|
2 |
imports Complex_Main |
46590 | 3 |
begin |
4 |
||
62290 | 5 |
section \<open>Arithmetics\<close> |
46590 | 6 |
|
7 |
declare [[quickcheck_finite_types = false]] |
|
8 |
||
9 |
find_unused_assms Divides |
|
10 |
find_unused_assms GCD |
|
51523 | 11 |
find_unused_assms Real |
46590 | 12 |
|
62290 | 13 |
section \<open>Set Theory\<close> |
46590 | 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 |
||
62290 | 22 |
section \<open>Datatypes\<close> |
46590 | 23 |
|
24 |
find_unused_assms List |
|
25 |
find_unused_assms Map |
|
26 |
||
46697
b07ae33cc459
removing Find_Unused_Assms_Examples from session as it requires much time
bulwahn
parents:
46673
diff
changeset
|
27 |
end |