author  traytel 
Mon, 24 Oct 2016 16:53:32 +0200  
changeset 64378  e9eb0b99a44c 
parent 62290  658276428cfc 
child 70118  62b875ba33e1 
permissions  rwrr 
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 