src/HOL/Quickcheck_Examples/Find_Unused_Assms_Examples.thy
author bulwahn
Wed, 22 Feb 2012 17:25:35 +0100
changeset 46590 0a28a5a97d71
child 46673 34e26d5119ef
permissions -rw-r--r--
adding some examples with find_unused_assms command
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46590
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
     1
theory Find_Unused_Assms_Examples
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
     2
imports Main
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
     3
begin
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
     4
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
     5
section {* Arithmetics *}
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
     6
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
     7
declare [[quickcheck_finite_types = false]]
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
     8
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
     9
find_unused_assms Divides
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    10
find_unused_assms GCD
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    11
find_unused_assms MacLaurin
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    12
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    13
section {* Set Theory *}
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    14
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    15
declare [[quickcheck_finite_types = true]]
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    16
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    17
find_unused_assms Fun
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    18
find_unused_assms Relation
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    19
find_unused_assms Set
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    20
find_unused_assms Wellfounded
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    21
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    22
section {* Datatypes *}
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    23
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    24
find_unused_assms List
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    25
find_unused_assms Map
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    26
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    27
end