isabelle: src/HOL/Library/Predicate_Compile_Quickcheck.thy@4d04e14d7ab8 (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
60500 903bb1495239 isabelle update_cartouches; wenzelm parents: 58881 diff changeset	3	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	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