author | nipkow |
Tue, 05 Nov 2019 21:07:03 +0100 | |
changeset 71044 | cb504351d058 |
parent 70119 | b48a496ca0cd |
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 |
|
70118 | 7 |
context notes [[quickcheck_finite_types = false]] |
8 |
begin |
|
9 |
find_unused_assms Divides |
|
10 |
find_unused_assms GCD |
|
11 |
find_unused_assms Real |
|
12 |
end |
|
46590 | 13 |
|
14 |
||
62290 | 15 |
section \<open>Set Theory\<close> |
46590 | 16 |
|
70118 | 17 |
context notes [[quickcheck_finite_types = true]] |
18 |
begin |
|
19 |
find_unused_assms Fun |
|
20 |
find_unused_assms Relation |
|
21 |
find_unused_assms Set |
|
22 |
find_unused_assms Wellfounded |
|
23 |
end |
|
46590 | 24 |
|
25 |
||
62290 | 26 |
section \<open>Datatypes\<close> |
46590 | 27 |
|
70118 | 28 |
context notes [[quickcheck_finite_types = true]] |
29 |
begin |
|
70119
b48a496ca0cd
more robust test: avoid spurious Interrupt (stack overflow?) due to List.fun_lub_parametric;
wenzelm
parents:
70118
diff
changeset
|
30 |
context notes [[quickcheck_finite_type_size = 2]] |
b48a496ca0cd
more robust test: avoid spurious Interrupt (stack overflow?) due to List.fun_lub_parametric;
wenzelm
parents:
70118
diff
changeset
|
31 |
begin |
b48a496ca0cd
more robust test: avoid spurious Interrupt (stack overflow?) due to List.fun_lub_parametric;
wenzelm
parents:
70118
diff
changeset
|
32 |
find_unused_assms List |
b48a496ca0cd
more robust test: avoid spurious Interrupt (stack overflow?) due to List.fun_lub_parametric;
wenzelm
parents:
70118
diff
changeset
|
33 |
end |
70118 | 34 |
find_unused_assms Map |
35 |
end |
|
46590 | 36 |
|
46697
b07ae33cc459
removing Find_Unused_Assms_Examples from session as it requires much time
bulwahn
parents:
46673
diff
changeset
|
37 |
end |