src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
changeset 70118 62b875ba33e1
parent 62290 658276428cfc
child 70119 b48a496ca0cd
     1.1 --- a/src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy	Thu Apr 11 12:18:03 2019 +0200
     1.2 +++ b/src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy	Thu Apr 11 12:38:22 2019 +0200
     1.3 @@ -4,24 +4,31 @@
     1.4  
     1.5  section \<open>Arithmetics\<close>
     1.6  
     1.7 -declare [[quickcheck_finite_types = false]]
     1.8 +context notes [[quickcheck_finite_types = false]]
     1.9 +begin
    1.10 +  find_unused_assms Divides
    1.11 +  find_unused_assms GCD
    1.12 +  find_unused_assms Real
    1.13 +end
    1.14  
    1.15 -find_unused_assms Divides
    1.16 -find_unused_assms GCD
    1.17 -find_unused_assms Real
    1.18  
    1.19  section \<open>Set Theory\<close>
    1.20  
    1.21 -declare [[quickcheck_finite_types = true]]
    1.22 +context notes [[quickcheck_finite_types = true]]
    1.23 +begin
    1.24 +  find_unused_assms Fun
    1.25 +  find_unused_assms Relation
    1.26 +  find_unused_assms Set
    1.27 +  find_unused_assms Wellfounded
    1.28 +end
    1.29  
    1.30 -find_unused_assms Fun
    1.31 -find_unused_assms Relation
    1.32 -find_unused_assms Set
    1.33 -find_unused_assms Wellfounded
    1.34  
    1.35  section \<open>Datatypes\<close>
    1.36  
    1.37 -find_unused_assms List
    1.38 -find_unused_assms Map
    1.39 +context notes [[quickcheck_finite_types = true]]
    1.40 +begin
    1.41 +  find_unused_assms List
    1.42 +  find_unused_assms Map
    1.43 +end
    1.44  
    1.45  end