src/HOL/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
author Christian Sternagel
Thu Aug 30 15:44:03 2012 +0900 (2012-08-30)
changeset 49093 fdc301f592c4
parent 48490 1959baa22632
child 51521 36fa825e0ea7
permissions -rw-r--r--
forgot to add lemmas
     1 theory Find_Unused_Assms_Examples
     2 imports Complex_Main
     3 begin
     4 
     5 section {* Arithmetics *}
     6 
     7 declare [[quickcheck_finite_types = false]]
     8 
     9 find_unused_assms Divides
    10 find_unused_assms GCD
    11 find_unused_assms RealDef
    12 find_unused_assms RComplete
    13 
    14 section {* Set Theory *}
    15 
    16 declare [[quickcheck_finite_types = true]]
    17 
    18 find_unused_assms Fun
    19 find_unused_assms Relation
    20 find_unused_assms Set
    21 find_unused_assms Wellfounded
    22 
    23 section {* Datatypes *}
    24 
    25 find_unused_assms List
    26 find_unused_assms Map
    27 
    28 end