isabelle: src/HOL/Library/SML_Quickcheck.thy@baf5953615da (annotated)

33084 cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	1
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	2	header {* Install quickcheck of SML code generator *}
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	3
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	4	theory SML_Quickcheck
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	5	imports Main
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	6	begin
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	7
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	8	setup {*
37390 8781d80026fc moved inductive_codegen to place where product type is available; tuned structure name haftmann parents: 33771 diff changeset	9	Inductive_Codegen.quickcheck_setup #>
39252 8f176e575a49 changing the container for the quickcheck options to a generic data bulwahn parents: 37390 diff changeset	10	Context.theory_map (Quickcheck.add_generator ("SML", Codegen.test_term))
33084 cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	11	*}
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	12
cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	13	end