src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
author traytel
Mon, 24 Oct 2016 16:53:32 +0200
changeset 64378 e9eb0b99a44c
parent 62290 658276428cfc
child 70118 62b875ba33e1
permissions -rw-r--r--
apply transfer_prover after folding relator_eq
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
46673
34e26d5119ef adding some more test invocations of find_unused_assms
bulwahn
parents: 46590
diff changeset
     2
imports Complex_Main
46590
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
62290
658276428cfc isabelle update_cartouches -c -t;
wenzelm
parents: 62286
diff changeset
     5
section \<open>Arithmetics\<close>
46590
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
51523
97b5e8a1291c rename RealDef to Real
hoelzl
parents: 51521
diff changeset
    11
find_unused_assms Real
46590
0a28a5a97d71 adding some examples with find_unused_assms command
bulwahn
parents:
diff changeset
    12
62290
658276428cfc isabelle update_cartouches -c -t;
wenzelm
parents: 62286
diff changeset
    13
section \<open>Set Theory\<close>
46590
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
62290
658276428cfc isabelle update_cartouches -c -t;
wenzelm
parents: 62286
diff changeset
    22
section \<open>Datatypes\<close>
46590
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
46697
b07ae33cc459 removing Find_Unused_Assms_Examples from session as it requires much time
bulwahn
parents: 46673
diff changeset
    27
end