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
bulwahn@46590
     1
theory Find_Unused_Assms_Examples
bulwahn@46673
     2
imports Complex_Main
bulwahn@46590
     3
begin
bulwahn@46590
     4
bulwahn@46590
     5
section {* Arithmetics *}
bulwahn@46590
     6
bulwahn@46590
     7
declare [[quickcheck_finite_types = false]]
bulwahn@46590
     8
bulwahn@46590
     9
find_unused_assms Divides
bulwahn@46590
    10
find_unused_assms GCD
bulwahn@46673
    11
find_unused_assms RealDef
bulwahn@46673
    12
find_unused_assms RComplete
bulwahn@46590
    13
bulwahn@46590
    14
section {* Set Theory *}
bulwahn@46590
    15
bulwahn@46590
    16
declare [[quickcheck_finite_types = true]]
bulwahn@46590
    17
bulwahn@46590
    18
find_unused_assms Fun
bulwahn@46590
    19
find_unused_assms Relation
bulwahn@46590
    20
find_unused_assms Set
bulwahn@46590
    21
find_unused_assms Wellfounded
bulwahn@46590
    22
bulwahn@46590
    23
section {* Datatypes *}
bulwahn@46590
    24
bulwahn@46590
    25
find_unused_assms List
bulwahn@46590
    26
find_unused_assms Map
bulwahn@46590
    27
bulwahn@46697
    28
end