isabelle: src/HOL/Quickcheck_Examples/Find_Unused_Assms_Examples.thy@e6b51fab96f7 (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	blanchet
	Mon, 21 May 2012 10:39:31 +0200
changeset 47944	e6b51fab96f7
parent 46697	b07ae33cc459
permissions	-rw-r--r--