isabelle: src/HOL/Library/Predicate_Compile_Quickcheck.thy@fd01ef524169 (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
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63992 diff changeset	11	ML_file \<open>../Tools/Predicate_Compile/predicate_compile_quickcheck.ML\<close>
48891 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	wenzelm
	Sun, 25 Aug 2024 22:54:56 +0200
changeset 80771	fd01ef524169
parent 69605	a96320074298
permissions	-rw-r--r--