src/HOL/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
author wenzelm
Wed Apr 10 21:20:35 2013 +0200 (2013-04-10)
changeset 51692 ecd34f863242
parent 51523 97b5e8a1291c
permissions -rw-r--r--
tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
declare command "print_case_translations" where it is actually defined;
     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 Real
    12 
    13 section {* Set Theory *}
    14 
    15 declare [[quickcheck_finite_types = true]]
    16 
    17 find_unused_assms Fun
    18 find_unused_assms Relation
    19 find_unused_assms Set
    20 find_unused_assms Wellfounded
    21 
    22 section {* Datatypes *}
    23 
    24 find_unused_assms List
    25 find_unused_assms Map
    26 
    27 end