isabelle: src/HOL/Library/Predicate_Compile_Quickcheck.thy@17a20ca86d62 (annotated)

63992 3aa9837d05c7 updated headers; wenzelm parents: 63764 diff changeset	1	(* Title: HOL/Library/Predicate_Compile_Quickcheck.thy
63764 f3ad26c4b2d9 tuned headers; wenzelm parents: 60500 diff changeset	2	Author: Lukas Bulwahn, TU Muenchen
f3ad26c4b2d9 tuned headers; wenzelm parents: 60500 diff changeset	3	*)
35953 0460ff79bb52 moved further predicate compile files to HOL-Library bulwahn parents: diff changeset	4
60500 903bb1495239 isabelle update_cartouches; wenzelm parents: 58881 diff changeset	5	section \<open>A Prototype of Quickcheck based on the Predicate Compiler\<close>
35953 0460ff79bb52 moved further predicate compile files to HOL-Library bulwahn parents: diff changeset	6
0460ff79bb52 moved further predicate compile files to HOL-Library bulwahn parents: diff changeset	7	theory Predicate_Compile_Quickcheck
63764 f3ad26c4b2d9 tuned headers; wenzelm parents: 60500 diff changeset	8	imports Predicate_Compile_Alternative_Defs
35953 0460ff79bb52 moved further predicate compile files to HOL-Library bulwahn parents: diff changeset	9	begin
0460ff79bb52 moved further predicate compile files to HOL-Library bulwahn parents: diff changeset	10
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 45450 diff changeset	11	ML_file "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 45450 diff changeset	12
51143 0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral; haftmann parents: 48891 diff changeset	13	end

author	hoelzl
	Fri, 30 Sep 2016 16:08:38 +0200
changeset 64008	17a20ca86d62
parent 63992	3aa9837d05c7
child 69605	a96320074298
permissions	-rw-r--r--