isabelle: src/HOL/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy@0a2371e7ced3 (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
46673 34e26d5119ef adding some more test invocations of find_unused_assms bulwahn parents: 46590 diff changeset	11	find_unused_assms RealDef
34e26d5119ef adding some more test invocations of find_unused_assms bulwahn parents: 46590 diff changeset	12	find_unused_assms RComplete
46590 0a28a5a97d71 adding some examples with find_unused_assms command bulwahn parents: diff changeset	13
0a28a5a97d71 adding some examples with find_unused_assms command bulwahn parents: diff changeset	14	section {* Set Theory *}
0a28a5a97d71 adding some examples with find_unused_assms command bulwahn parents: diff changeset	15
0a28a5a97d71 adding some examples with find_unused_assms command bulwahn parents: diff changeset	16	declare [[quickcheck_finite_types = true]]
0a28a5a97d71 adding some examples with find_unused_assms command bulwahn parents: diff changeset	17
0a28a5a97d71 adding some examples with find_unused_assms command bulwahn parents: diff changeset	18	find_unused_assms Fun
0a28a5a97d71 adding some examples with find_unused_assms command bulwahn parents: diff changeset	19	find_unused_assms Relation
0a28a5a97d71 adding some examples with find_unused_assms command bulwahn parents: diff changeset	20	find_unused_assms Set
0a28a5a97d71 adding some examples with find_unused_assms command bulwahn parents: diff changeset	21	find_unused_assms Wellfounded
0a28a5a97d71 adding some examples with find_unused_assms command bulwahn parents: diff changeset	22
0a28a5a97d71 adding some examples with find_unused_assms command bulwahn parents: diff changeset	23	section {* Datatypes *}
0a28a5a97d71 adding some examples with find_unused_assms command bulwahn parents: diff changeset	24
0a28a5a97d71 adding some examples with find_unused_assms command bulwahn parents: diff changeset	25	find_unused_assms List
0a28a5a97d71 adding some examples with find_unused_assms command bulwahn parents: diff changeset	26	find_unused_assms Map
0a28a5a97d71 adding some examples with find_unused_assms command bulwahn parents: diff changeset	27
46697 b07ae33cc459 removing Find_Unused_Assms_Examples from session as it requires much time bulwahn parents: 46673 diff changeset	28	end

author	haftmann
	Fri, 15 Feb 2013 08:31:31 +0100
changeset 51143	0a2371e7ced3
parent 48490	1959baa22632
child 51521	36fa825e0ea7
permissions	-rw-r--r--