src/HOL/Quickcheck_Examples/Find_Unused_Assms_Examples.thy
author huffman
Sun Apr 01 16:09:58 2012 +0200 (2012-04-01)
changeset 47255 30a1692557b0
parent 46697 b07ae33cc459
permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
     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