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
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