| author | eberlm | 
| Fri, 26 Feb 2016 11:57:36 +0100 | |
| changeset 62424 | 8c47e7fcdb8d | 
| 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: 
46590diff
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: 
46673diff
changeset | 27 | end |