isabelle: src/HOL/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy@97b5e8a1291c (annotated)

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
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
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
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
46697 b07ae33cc459 removing Find_Unused_Assms_Examples from session as it requires much time bulwahn parents: 46673 diff changeset	27	end

author	hoelzl
	Tue, 26 Mar 2013 12:20:56 +0100
changeset 51523	97b5e8a1291c
parent 51521	36fa825e0ea7
permissions	-rw-r--r--