isabelle: src/HOL/Library/SML_Quickcheck.thy@4e2aaf080572 (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 #>
33084 cd1579e0997a turned off old quickcheck haftmann parents: diff changeset	10	Quickcheck.add_generator ("SML", Codegen.test_term)
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