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

35953 0460ff79bb52 moved further predicate compile files to HOL-Library bulwahn parents: diff changeset	1	(* Author: Lukas Bulwahn, TU Muenchen *)
0460ff79bb52 moved further predicate compile files to HOL-Library bulwahn parents: diff changeset	2
58881 b9556a055632 modernized header; wenzelm parents: 58812 diff changeset	3	section {* A Prototype of Quickcheck based on the Predicate Compiler *}
35953 0460ff79bb52 moved further predicate compile files to HOL-Library bulwahn parents: diff changeset	4
0460ff79bb52 moved further predicate compile files to HOL-Library bulwahn parents: diff changeset	5	theory Predicate_Compile_Quickcheck
0460ff79bb52 moved further predicate compile files to HOL-Library bulwahn parents: diff changeset	6	imports Main Predicate_Compile_Alternative_Defs
0460ff79bb52 moved further predicate compile files to HOL-Library bulwahn parents: diff changeset	7	begin
0460ff79bb52 moved further predicate compile files to HOL-Library bulwahn parents: diff changeset	8
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 45450 diff changeset	9	ML_file "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 45450 diff changeset	10
51143 0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral; haftmann parents: 48891 diff changeset	11	end